Using Assumptions to Distribute Alternation Free μ-Calculus Model Checking

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.