2001 | OriginalPaper | Buchkapitel
Distributed Symbolic Model Checking for μ-Calculus
verfasst von : Orna Grumberg, Tamir Heyman, Assaf Schuster
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
In this paper we propose a distributed symbolic algorithm for model checking of propositional μ-calculus formulas. μ-calculus is a powerful formalism and many problems like (fair) CTL and LTL model checking can be solved using the μ-calculus model checking. Previous works on distributed symbolic model checking were restricted to reachability analysis and safety properties. This work thus significantly extends the scope of properties that can be verified for very large designs.The algorithm distributively evaluates subformulas. It results in sets of states which are evenly distributed among the processes.We show that this algorithm is scalable, and thus can be implemented on huge distributed clusters of computing nodes. In this way, the memory modules of the computing nodes collaborate to create a very large store, thus enables the checking of much larger designs. We formally prove the correctness of the parallel algorithm. We complement the distribution of the state sets by showing how to distribute the transition relation.