Abstract
It is often the case that systems are “nearly symmetric”; they exhibit symmetry in a part of their description but are, nevertheless, globally asymmetric. We formalize several notions of near symmetry and show how to obtain the benefits of symmetry reduction when applied to asymmetric systems which are nearly symmetric. We show that for some nearly symmetric systems it is possible to perform symmetry reduction and obtain a bisimilar (up to permutation) symmetry reduced system.Using a more general notion of “sub-symmetry” we show how to generate a reduced structure that is simulated (up to permutation) by the original asymmetric program.
In the symbolic model checking paradigm, representing the symmetry reduced quotient structure entails representing the BDD for the orbit relation. Unfortunately, for many important symmetry groups, including the full symmetry group, this BDD is provably always intractably large, of size exponential in the number of bits in the state space. In contrast, under the assumption of full symmetry, we show that it is possible to reduce a textual program description of a symmetric system to a textual program description of the symmetry reduced system. This obviates the need for building the BDD representation of the orbit relation on the program states under the symmetry group. We establish that the BDD representing the reduced program is provably small, essentially polynomial in the number of bits in the state space of the original program.
Acknowledgment
The authors would like to thank Bob Kurshan for many stimulating comments and discussions.
The authors’ work was supported in part by NSF grant CCR-980-4736 and SRC contract 98-DP-388.
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
Ajami, K., Haddad, S. and Ilie, J.-M., Exploiting Symmetry in Linear Time Temporal Logic Model Checking: One Step Beyond. In Tools and Algorithms for the Construction and Analysis of Systems, 4th Interntational Conference, ETAPS98 LNCS 1384, Springer Verlag, 1998.
Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L. and Hwang, L. J., Symbolic Model Checking: 102 states and beyond. In Information and Computation, 98(2):142–170, June, 1992.
Bryant, R. E., Graph-Based Algorithms for Boolean Function Manipulation. In IEEE Transactions on Computers, Vol. C-35, No. 8, Aug. 86, pp. 677–691.
Clarke, E. M., and Emerson, E. A., Design and Verification of Synchronization Skeletons using Branching Time Temporal Logic. In Logics of Programs Workshop, Springer, LNCS no. 131., pp. 52–71, May 1981.
Clarke, E. M., Emerson, E. A., Jha, S. and Sistla A. P., Symmetry Reductions in Model Checking. In Computer Aided Verification, 10th International Conference LNCS 1427, Springer-Verlag, 1998.
Clarke, E. M., Emerson, E. A., and Sistla, A. P., Automatic Verification of Finite State Concurrent System Using Temporal Logic. In ACM Trans. on Prog. Lang. and Sys., vol. 8, no. 2, pp. 244–263, April 1986.
Clarke, E. M., Enders, R., Filkorn, T., and Jha, S., Exploiting Symmetry in Temporal Logic Model Checking. In Formal Methods in System Design, Kluwer, vol. 9, no. 1/2, August 1996.
Clarke, E. M., Grumberg, O. and Long, D. E., Model Checking and Abstraction. In Transactions on Programming Languages and Systems ACM, vol 16, no. 5, 1994.
E. Allen Emerson, Temporal and Modal Logic. In J. van Leeuwen editor Handbook of Theoretical Computer Science vol. B, Elsevier Science Publishing, 1990.
Emerson, E. A., and Halpern, J. Y., ’sometimes’ and ‘Not Never’ Revisited: On Branching versus Linear Time Temporal Logic, JACM, vol. 33, no. 1, pp. 151–178, Jan. 86.
Emerson, E. A. and Sistla, A. P., Symmetry and Model Checking. In Formal Methods in System Design, Kluwer, vol. 9, no. 1/2, August 1996.
Emerson, E. A. and Sistla, A. P., Utilizing Symmetry when Model Checking under Fairness Assumptions. In TOPLAS 19(4): 617–638 (1997).
Emerson, E. A. and Trefler, R. J., Model Checking Real-Time Properties of Symmetric Systems. In Mathematical Foundations of Computer Science, 23rd International Symposium LNCS 1450, Springer-Verlag, 1998.
Gyuris, V. and Sistla, A. P., On-the-Fly Model checking under Fairness that Exploits Symmetry. In Proceedings of the 9th International Conference on Computer Aided Verification, Haifa, Israel, 1997.
Haddad, S., Ilie, J. M., Taghelit, M. and Zouari, B., Symbolic Reachability Graph and Partial Symmetries. In Application and Theory of Petri Nets 1995, Springer-Verlag, LNCS 935, 1995.
Hennessy, M., Milner, R., Algebraic Laws for Nondeterminism and Concurrency. In Journal of the ACM, Vol 32, no. 1, January, 1985, pp 137–161.
Ip, C-W. N., Dill, D. L., Better Verification through Symmetry. In Formal Methods in System Design, Kluwer, vol. 9, no. 1/2, August 1996.
Jensen, K. and Rozenberg, G. (eds.), High-Level Petri Nets: Theory and Application, Springer-Verlag, 1991.
Kohavi, Zvi, Switching and Finite Automata Theory, second edition, McGraw-Hill Book Company, New York, 1978.
Lichtenstein, O., and Pnueli, A., Checking That Finite State Concurrent Programs Satisfy Their Linear Specifications, POPL85, pp. 97–107, Jan. 85.
Michel, F., Azema, P. and Vernadat, F., Permutable Agents in Process Algebra. In Tools and Algorithms for the Construction and Analysis of Systems, 96, Springer Verlag, LNCS 1055, 1996.
Milner, R., An Algebraic Definition of Simulations Between Programs. In Proceedings of the Second International Joint Conference on Artificial Intelligence, British Computer Society, 1971, pp 481–489.
McMillan, K. L., Symbolic Model Checking: An Approach to the State Explosion Problem, Ph.D. Thesis, Carnegie Mellon University, 1992.
Park, D., Concurrency and Automata on Infinite Sequences. In Theoretical Computer Science: 5th GI-Conference, Karlsruhe, Springer-Verlag, LNCS 104, pp 167–183, 1981.
Queille, J. P., and Sifakis, J., Specification and verification of concurrent programs in CESAR, Proc. 5th Int. Symp. Prog., Springer LNCS no. 137, pp. 195–220, 1982.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Emerson, E.A., Trefler, 1.J. (1999). From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking. In: Pierre, L., Kropf, T. (eds) Correct Hardware Design and Verification Methods. CHARME 1999. Lecture Notes in Computer Science, vol 1703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48153-2_12
Download citation
DOI: https://doi.org/10.1007/3-540-48153-2_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66559-5
Online ISBN: 978-3-540-48153-9
eBook Packages: Springer Book Archive