Employing symmetry reductions in model checking. (English) Zbl 1072.68068

Summary: This paper presents a survey of research work that has been done over the last decade on exploiting symmetry in model checking of concurrent systems. It describes the techniques based on quotient structures, annotated quotient structures and guarded quotient structures. It also briefly describes some of the implemented systems.


68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B44 Temporal logic
Full Text: DOI


[1] Emerson, E. A.; Sistla, A. P., Symmetry and model checking. Fifth International Conference on Computer Aided Verification. Crete, Greece, June 1993, Journal Formal Methods in System Design, 9, 1/2, 105-130 (1996)
[2] Ip, C. N.; Dill, D. L., Better verification through symmetry. International Symposium on Computer Hardware Description Languages and their Application, April 1993, Formal Methods in System Design, 9, 1/2, 41-75 (1996)
[4] Sistla, A. P.; Gyuris, V.; Emerson, E. A., SMCa symmetry based model checker for safety and liveness properties, ACM Transactions on Software Engineering Methodologies, 9, 2, 133-166 (2000)
[10] Emerson, E. A., Temporal and modal logic, (van Leeuwen, J., Handbook of theoretical computer science (1991), Elsevier/North-Holland: Elsevier/North-Holland Amsterdam) · Zbl 0900.03030
[11] Manna, Z.; Pnueli, A., Temporal logic of reactive and concurrent systems: specification (1992), Springer: Springer Berlin
[16] Emerson, E. A.; Lei, C.-. L., Modalities for model checkingbranching time strikes back, Science of Computer Programming, 8, 275-306 (1987) · Zbl 0615.68019
[17] Aho, A. V.; Hopcroft, J.; Ullman, J. D., The design and analysis of computer algorithms (1974), Addison-Wesley: Addison-Wesley Reading, MA · Zbl 0326.68005
[22] Clarke, E. M.; Enders, R.; Filkorn, T.; Jha, S., Exploiting symmetry in temporal logic model checking, Formal Methods in System Design, 9, 1/2 (1996)
[23] Emerson, E. A.; Sistla, A. P., Utilizing symmetry when model checking under fairness assumptionsan automata-theoretic approach. Seventh International Conference on Computer Aided Verification, Leige, Belgium, July 1995, ACM Transactions on Programming Languages and Systems, 19, 4, 617-638 (1997)
[24] Kurshan, R. P., Computer aided verification of coordinated processes: the automata theoretic approach (1994), Princeton University Press: Princeton University Press Princeton, NJ
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.