Abstract
Model checking is a useful technique to verify properties of dynamic systems but it has to cope with the state explosion problem. By simultaneous exploitation of symmetries of both the system and the property, the model checking can be performed on a reduced quotient structure [2,6,7]. In these techniques a property is specified within a temporal logic formula (CTL*) and the symmetries of the formula are obtained by a syntactical checking. We show here that these approaches fail to capture symmetries in the LTL path subformulas. Thus we propose a more accurate method based on local symmetries of the associated Büchi automaton. We define an appropriate quotient structure for the synchronized product of the Büchi automaton and the global state transition graph. We prove that model checking can be performed over this quotient structure leading to efficient algorithms.
Chapter PDF
References
G. Chiola, C. Dutheillet, G. Franceschinis, S. Haddad, “On Well-formed Colored Nets and their Symbolic Reachability Graph”, proc. of 11th International Conference on Application and Theory of Petri Nets, Paris-France, June 1990.
E. Clarke, T. Filkorne, S. Jha, “Exploiting Symmetry In Temporal Logic Model Checking”, 5th Computer Aided Verification (CAV), June 1993.
E. Clarke, O. Grumberg, D. Long,“Verification Tools for Finit-State Concurrent Systems”, “A Decade of Concurrency-Reflections and Perspectives”, LNCS vol 803, 1994.
C. Courcoubetis, M. Vardi, P.Wolper, M. Yannakakis, “Memory Efficient Algorithms for the Verification of Temporal Properties”, In proceedings of CAV'90, North Holland, DIMACS 30. 1990.
M. Dam. “Fixed points of Büchi automata”, In R. Shymanasundar, editor, Foundations of Software Technology and theoretical Computer Science, volume 652 of LNCS, pages 39–50, Springer-Verlag, 1992.
E.A. Emerson, A. Prasad Sistla, “Symmetry and Model Checking”, In Formal Methods and System Design 9, pp 105–131, 1996.
E.A. Emerson, A. Prasad Sistla, “Symmetry and Model Checking”, 5th conference on Computer Aided Verification (CAV), June 1993.
E.A. Emerson, A. Parsad Sistla, “Utilizing Symmetry when Model Checking under Fairness Assumptions: An Automata-theoric Approach”, 7th CAV, LNCS 939, pp. 309–324, Liège, Belgium, July 1995.
E.A. Emerson, “Temporal and Modal Logic”, HandBook of Theoretical Computer Science, Volume B, J. van Leeuwen (eds), 1990.
E.A. Emerson and Chin-Laung Lei, “Modalities for Model Checking: Branching Time Stricks Back”, In Proc of 12h Annual Symposium on Principles of Programming Languages, New-Orleans, Louisiana, January 1985.
R. Gerth, D. Peled, M. Vardi, P. Wolper, “Simple On-the-fly Automatic Verification of linear Temporal Logic”, Protocol Specification Testing and Verification, 1995, Warsaw, Poland.
S. Haddad, JM. Ilié, B. Zouari, M. Taghelit, “Symbolic Reachability Graph and Partial Symmetries”, In Proc. of the 16th ICATPN, Torino, Italy, June 1995.
J-M. Ilié, K. Ajami, “Model Checking through the Symbolic Reachability Graph”, in Proc of TapSoft'97 — CAAP, pp 213–224, Lille, France, Springer-Verlag, LNCS 1214, Avril 1997.
K. Jensen, G. Rozenberg (eds), “High Level Petri Nets, Theory and Application”, Springer-Verlag, 1991.
Z. Manna, A. Pnueli. “The Temporal Logic of Reactive and Concurrent Systems: Specification”, Springer-Verlag, 1992.
F. Michel, P. Azéma, F. Vernadat. “Permutable Agents and Process Algebra”, In Proc. of TACAS'96, Passau, Germany, 1996, Springer-Verlag, LNCS 1055.
C. Norris IP and D. Dill, “Better Verification Through Symmetry”, In Formal Methods in System Design, Vol 9, August 96, pp 41–76.
D. Park, “Concurrency and Automata on Infinite Sequences”, LNCS vol 114, 1984.
K. Schmidt, “Symmetry Calculation”, Workshop CSP Warschau 1995.
M.Y. Vardi, “Alternating Automata and Program Verification”, Computer Science Today: Recent Trends and Developments.LNCS,Vol. 1000, Springer-Verlag 1995.
M. Y. Vardi, “An Automata-theoretic approach to linear temporal logic (banff' 94), LNCS, 1043, 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ajami, K., Haddad, S., Ilié, J.M. (1998). Exploiting symmetry in linear time temporal logic model checking: One step beyond. In: Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1998. Lecture Notes in Computer Science, vol 1384. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054164
Download citation
DOI: https://doi.org/10.1007/BFb0054164
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64356-2
Online ISBN: 978-3-540-69753-4
eBook Packages: Springer Book Archive