Abstract
We show how to exploit symmetry in model checking for concurrent systems containing many identical or isomorphic components. We focus in particular on those composed of many isomorphic processes. In many cases we are able to obtain significant, even exponential, savings in the complexity of model checking.
The work of the first author was supported in part by ONR contract N00014-89-J-1472, and Texas Advanced Technology Program Grant 003658-250. The work of the second author was supported in part by NSF grant CCR-9212183.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Aggarwal S., Kurshan R. P., Sabnani K. K., ”A Calculus for Protocol Specification and Validation”, in Protocol Specification, Testing and Verification III, H. Ruden, C. West (ed's), North-Holland 1983, 19–34.
Attie, P. C., and Emerson, E. A., Synthesis of Many Processes, POPL89
Clarke, E. M., and Emerson, E. A., Design and Verification of Synchronization Skeletons using Branching Time Temporal Logic. Logics of Programs Workshop 1981, Springer LNCS no. 131.
Clarke, E. M., Filkorn, T., Jha, S. Exploiting Symmetry in Temporal Logic Model Checking, 5th CAV, June 1993 (this proceedings).
Clarke, E. M., Grumberg, O., and Brown, M., Characterizing Kripke Structures in Temporal Logic, Theor. Comp. Sci., 1988
Clarke, E. M., Grumberg, O., and Brown, M., Reasoning about Many Identical Processes, Inform. and Comp., 1989
Emerson, E. A., and Clarke, E. M., Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons, Science of Computer Programming, Dec 1982.
Emerson, E. A., Temporal and Modal Logic, in Handbook of Theoretical Computer Science, (J. van Leeuwen, ed.), Elsevier/North-Holland, 1991.
Herstein, 1, Topics in Algebra, Xerox 196?
Hoffmann, C. Graph Isomorphism and Permutation Groups. Springer LNCS, 1992.
Kurshan, R. P., ”Testing Containment of omega-regular Languages”, Bell Labs Tech. Report. 1121-861010-33 (1986); conference version in R. P. Kurshan, ”Reducibility in Analysis of Coordination”, LNCIS 103 (1987) Springer-Verlag 19–39.
Jensen, K., and Rozenberg, G. (eds.), High-level Petri Nets: Theory and Application, Springer-Verlag, 1991.
Kohavi, Z., Switching and Finite Automata Theory, McGraw-Hill, 1978.
Ip, C-W. N., Dill, D. L., Better Verification through Symmetry, CHDL, April 1993.
Manna, Z. and Pnueli, A., Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, 1992
Stirling, C., Modal and Temporal Logics. in Handbook of Logic in Computer Science, (D. Gabbay, ed.) Oxford, 1993
Weyl, H., Symmetry, Princeton Univ. Press, 1952
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Emerson, E.A., Sistla, A.P. (1993). Symmetry and model checking. In: Courcoubetis, C. (eds) Computer Aided Verification. CAV 1993. Lecture Notes in Computer Science, vol 697. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56922-7_38
Download citation
DOI: https://doi.org/10.1007/3-540-56922-7_38
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56922-0
Online ISBN: 978-3-540-47787-7
eBook Packages: Springer Book Archive