Advertisement

From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking

  • E. Allen Emerson
  • 1]Richard J. Trefler
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1703)

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.

Keywords

Model Check Critical Section Symmetry Reduction Kripke Structure Orbit Relation 
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

  1. AHI98.
    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.Google Scholar
  2. BC+92.
    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.zbMATHCrossRefMathSciNetGoogle Scholar
  3. Br86.
    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.Google Scholar
  4. CE81.
    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.CrossRefGoogle Scholar
  5. CE+98.
    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.CrossRefGoogle Scholar
  6. CES86.
    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.zbMATHCrossRefGoogle Scholar
  7. CE+96.
    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.Google Scholar
  8. CGL94.
    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.Google Scholar
  9. Em90.
    E. Allen Emerson, Temporal and Modal Logic. In J. van Leeuwen editor Handbook of Theoretical Computer Science vol. B, Elsevier Science Publishing, 1990.Google Scholar
  10. EH86.
    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.Google Scholar
  11. ES96.
    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.Google Scholar
  12. ES97.
    Emerson, E. A. and Sistla, A. P., Utilizing Symmetry when Model Checking under Fairness Assumptions. In TOPLAS 19(4): 617–638 (1997).CrossRefGoogle Scholar
  13. ET98.
    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.Google Scholar
  14. GS97.
    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.Google Scholar
  15. HI+95.
    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.Google Scholar
  16. HM85.
    Hennessy, M., Milner, R., Algebraic Laws for Nondeterminism and Concurrency. In Journal of the ACM, Vol 32, no. 1, January, 1985, pp 137–161.zbMATHCrossRefMathSciNetGoogle Scholar
  17. ID96.
    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.Google Scholar
  18. JR91.
    Jensen, K. and Rozenberg, G. (eds.), High-Level Petri Nets: Theory and Application, Springer-Verlag, 1991.Google Scholar
  19. Ko78.
    Kohavi, Zvi, Switching and Finite Automata Theory, second edition, McGraw-Hill Book Company, New York, 1978.zbMATHGoogle Scholar
  20. LP85.
    Lichtenstein, O., and Pnueli, A., Checking That Finite State Concurrent Programs Satisfy Their Linear Specifications, POPL85, pp. 97–107, Jan. 85.Google Scholar
  21. MAV96.
    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.Google Scholar
  22. Mi71.
    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.Google Scholar
  23. Mc92.
    McMillan, K. L., Symbolic Model Checking: An Approach to the State Explosion Problem, Ph.D. Thesis, Carnegie Mellon University, 1992.Google Scholar
  24. Pa81.
    Park, D., Concurrency and Automata on Infinite Sequences. In Theoretical Computer Science: 5th GI-Conference, Karlsruhe, Springer-Verlag, LNCS 104, pp 167–183, 1981.Google Scholar
  25. QS82.
    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.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • E. Allen Emerson
    • 1
  • 1]Richard J. Trefler
  1. 1.Department of Computer Sciences and Computer Engineering Research CenterUniversity of TexasTXUSA

Personalised recommendations