Abstract
In this paper we propose a distributed symbolic algorithm for model checking of propositional μ-calculus formulas. μ-calculus is a powerful formalism and μ-calculus model checking can solve many problems, including, for example, verification of (fair) CTL and LTL properties. 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 distributively, enabling us to use them 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 therefore can be implemented on huge distributed clusters of computing nodes. The memory modules of the computing nodes collaborate to create a very large memory space, thus enabling 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.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
S. Ben-David, O. Grumberg, T. Heyman, and A. Schuster, “Scalable distributed on-the-fly symbolic model checking,” Software Tools for Technology Transfer, Vol. 4 No. 4, pp. 496–504, 2003.
R.E. Bryant, “Graph-based algorithms for boolean function manipulation,” IEEE Transactions on Computers, Vol. C-35, No. 8, pp. 677–691, 1986.
J.R. Burch, E.M. Clarke, and D.E. Long, “Symbolic model checking with partitioned transition relations,” in A. Halaas and P.B. Denyer (Eds.), Proceedings of the 1991 International Conference on Very Large Scale Integration, August 1991.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang, “Symbolic model checking: 1020 states and beyond,” Information and Computation, Vol. 98, No. 2, pp. 142–171, 1992. Special Issue: Selections from 1990 IEEE Symposium on Logic in Computer Science.
G. Cabodi, P. Camurati, and S. Quer, “Improving the Efficient of BDD-bsaed operators by means of partitioning,” IEEE Transactions on Computer-Aided Design, May 1999, pp. 545–556.
E.M. Clarke, E.A. Emerson, and A.P. Sistla, “Automatic verification of finite-state concurrent systems using temporal logic specifications,” in Proceedings of the Tenth Annual ACM Symposium on Principles of Programming Languages, January 1983.
E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking, MIT press, December 1999.
R. Cleaveland, “Tableau-based model checking in the propositional μ-calculus,” Acta Informatica, Vol. 27, pp. 725–747, 1990.
O. Coudert, J.C. Madre, and C. Berthet, “Verifying of synchronous sequential machines based on symbolic execution,” in J. Sifakis (Ed), Workshop on Automatic Verification Methods for Finite State Systems, Springer-Verlag: Grenoble, France, 1989, pp. 365–373.
E.A. Emerson and C.-L. Lei, “Efficient model checking in fragments of the propositional Mu-calculus,” in Proceedings of the First Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, June 1986.
Message Passing Interface Forum. MPI: A Message-Passing Interface standard. The International Journal of Supercomputer Applications and High Performance Computing, Vol. 8, 1994.
T. Heyman, D. Geist, O. Grumberg, and A. Schuster, “Achieving scalability in parallel reachability analysis of very large circuits,” in Proc. of the 12th International Conference on Computer Aided Verification, LNCS, 2000.
T. Heyman, D. Geist, O. Grumberg, and A. Schuster, “Achieving scalability in parallel reachability analysis of very large circuits,” Formal Methods in System Design, Vol. 21, No. 2, pp. 317–338, 2002.
D. Kozen, Results on the propositional μ-calculus, TCS, 27, 1983.
O. Lichtenstein and A. Pnueli, “Checking that finite state concurrent programs satisfy their linear specification,” in Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, January 1985, pp. 97–107.
D. Long, A. Browne, E. Clark, S. jha, and W. Marrero, “An improved algorithm for the evaluation of fixpoint expressions,” in Proc. of the Sixth International Conference on Computer Aided Verification, LNCS 818, 1994, pp. 338–350.
A. Narayan, A. Isles, J. Jain, R. Brayton, and A.L. Sangiovanni-Vincentelli, “Reachability analysis using partitioned-ROBDDs,” in Proceedings of the IEEE International Conference on Computer Aided Design, IEEE Computer Society Press, June 1997, pp. 388–393.
A. Narayan, J. Jain, M. Fujita, and A.L. Sangiovanni-Vincentelli, “Partitioned-ROBDDs,” in Proceedings of the IEEE International Conference on Computer Aided Design, IEEE Computer Society Press, June 1996, pp. 547–554.
J.P. Quielle and J. Sifakis, “Specification and verification of concurrent systems in CESAR,” in Proceedings of the Fifth International Symposium in Programming, 1981.
C. Stirling and D.J. Walker, “Local model checking in the model mu-calculus,” in Proc. of the 1989 Int. Joint Conf. on Theory and Practice of Software Development, 1989.
A. Tarski, “A lattice-theoretical fixpoint theorem and its applications,” Pacific J. Math, Vol. 5, pp. 285–309, 1955.
G. Winskel, “Model checking in the modal μ-calculus,” in Proceedings of the Sixteenth International Colloquium on Automata, Languages, and Programming, 1989.
Author information
Authors and Affiliations
Corresponding author
Additional information
This research was supported by The Israel Science Foundation (grant number 111/01-2) and by a grant from Intel Academic Relations.
Rights and permissions
About this article
Cite this article
Grumberg, O., Heyman, T. & Schuster, A. Distributed Symbolic Model Checking for μ-Calculus. Form Method Syst Des 26, 197–219 (2005). https://doi.org/10.1007/s10703-005-1493-1
Received:
Revised:
Accepted:
Issue Date:
DOI: https://doi.org/10.1007/s10703-005-1493-1