Abstract
When analyzing concurrent software applications, symmetry reduction techniques dramatically narrow the size of the state space search by identifying computations that, because of symmetries in the system, are redundant. While analysis algorithms exploiting symmetry reduction are well developed, little has been done in discovering the nature of the symmetries of a system. What is even less researched is discovering symmetries that are particular to a temporal property. This paper proposes a general framework for discovering symmetries in systems that exhibit absolute or relative symmetries depending on the property of interest. Our work extends previous symmetry reduction techniques by making advances in automating generalized model automorphism discovery. Generalized model automorphisms capture exact abstractions and therefore preserve both the validity and the violation of any property of the analyzed system while achieving dramatic state space reduction.
This research was sponsored by NSF under contract number SA4102-10097PG/CCR-0325274.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Cognitive agent architecture (Cougaar) open source project. http://www.cougaar.org
Ajami, K., Haddad, S., Ilié, J.-M.: Exploiting symmetry in linear time temporal logic model checking: One step beyond. In: Steffen, B. (ed.) ETAPS 1998 and TACAS 1998. LNCS, vol. 1384, pp. 52–62. Springer, Heidelberg (1998)
Clarke, E.M., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 450–462. Springer, Heidelberg (1993)
Ip, C.N., Dill, D.L.: Verifying systems with replicated components in Murphi. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 147–158. Springer, Heidelberg (1996)
Courcoubetis, C. (ed.): CAV 1993. LNCS, vol. 697. Springer, Heidelberg (1993)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: popl77, Jan. 1977, pp. 238–252. ACM Press, New York (1977)
Emerson, E., Havlicek, J., Trefler, R.: Virtual symmetry reduction. In: 15th Symposium on Logic in Computer Science (LICS’ 00), Washington - Brussels - Tokyo, June 2000, pp. 121–131. IEEE Computer Society Press, Los Alamitos (2000)
Emerson, E.A., Sistla, A.P.: Symmetry and model checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 463–478. Springer, Heidelberg (1993)
Emerson, E.A., Trefler, R.J.: From asymmetry to full symmetry: New techniques for symmetry reduction in model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 142–156. Springer, Heidelberg (1999)
Ganesh, V., Shankar, N., Saïdi, H.: Slicing SAL. Technical report, Computer Science Laboratory, SRI International, Menlo Park, CA (1999)
Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
Hamon, G., DeMoura, L., Rushby, J.: Generating efficient test sets with a model checker. In: 2nd International Conference on Software Engineering and Formal Methods, Beijing, China, Sept. 2004, pp. 261–270. IEEE Computer Society Press, Los Alamitos (2004)
Saïdi, H.: Model-checking guided abstraction and analysis. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 377–396. Springer, Heidelberg (2000)
Sistla, Gyuris, Emerson: SMC: A symmetry-based model checker for verification of safety and liveness properties. ACMTSEM: ACM Transactions on Software Engineering and Methodology 9 (2000)
Sistla, A.P., Gedefroid, P.: Symmetry and reduced symmetry in model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 91–103. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Saïdi, H. (2007). Discovering Symmetries. In: Brim, L., Haverkort, B., Leucker, M., van de Pol, J. (eds) Formal Methods: Applications and Technology. PDMC 2006. Lecture Notes in Computer Science, vol 4346. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70952-7_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-70952-7_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70951-0
Online ISBN: 978-3-540-70952-7
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science
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.
