Using Assumptions to Distribute Alternation Free μ-Calculus Model Checking |
| |
Authors: | Lubo Brim,Jitka
í dkov |
| |
Affiliation: | aFaculty of Informatics, Masaryk University Brno, Czech Republic |
| |
Abstract: | In this work we extend the approach used in [6] to perform distributed-memory AFMC model checking. The part of a system held in one computer is modeled as a Kripke structure with border states. Moreover, we use assumptions about the truth of a formula in each state. Each process then repeatedly executes a slight modification of a standard sequential algorithm and exchanges its results with other processes. In the paper we define the AFMC semantics for structures with border states and assumptions, present the distributed algorithm and show the main ideas behind the proof of its correctness. Complexity and experimental results are provided as well. |
| |
Keywords: | |
本文献已被 ScienceDirect 等数据库收录! |
|