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

## 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## References

- 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 - BC+92.Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L. and Hwang, L. J., Symbolic Model Checking: 10
^{2}states and beyond. In*Information and Computation*, 98(2):142–170, June, 1992.zbMATHCrossRefMathSciNetGoogle Scholar - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - 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 - JR91.Jensen, K. and Rozenberg, G. (eds.), High-Level Petri Nets: Theory and Application, Springer-Verlag, 1991.Google Scholar
- Ko78.Kohavi, Zvi,
*Switching and Finite Automata Theory*, second edition, McGraw-Hill Book Company, New York, 1978.zbMATHGoogle Scholar - LP85.Lichtenstein, O., and Pnueli, A., Checking That Finite State Concurrent Programs Satisfy Their Linear Specifications, POPL85, pp. 97–107, Jan. 85.Google Scholar
- 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 - 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 - Mc92.McMillan, K. L.,
*Symbolic Model Checking: An Approach to the State Explosion Problem*, Ph.D. Thesis, Carnegie Mellon University, 1992.Google Scholar - 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 - 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