Exploiting Symmetry in Linear Time Temporal Logic Model Checking : One Step Beyond
Ajami, Khalil; Haddad, Serge; Ilié, Jean-Michel (1998), Exploiting Symmetry in Linear Time Temporal Logic Model Checking : One Step Beyond, in Steffen, Bernhard, Tools and Algorithms for the Construction and Analysis of Systems. 4th International Conference, TACAS'98, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings, Springer : Berlin, p. 52-67. http://dx.doi.org/10.1007/BFb0054164
Type
Communication / ConférenceDate
1998Conference title
4th International Conference on Tools and Algorithms for the construction and Analysis of Systems (TACAS'98)Conference date
1998-03Conference city
LisbonneConference country
PortugalBook title
Tools and Algorithms for the Construction and Analysis of Systems. 4th International Conference, TACAS'98, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, ProceedingsBook author
Steffen, BernhardPublisher
Springer
Series title
Lecture Notes in Computer ScienceSeries number
1384Published in
Berlin
ISBN
978-3-540-64356-2
Number of pages
457Pages
52-67
Publication identifier
Metadata
Show full item recordAbstract (EN)
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.Subjects / Keywords
LTL; Temporal Logic; Symmetries; Büchi automata; Model Checking; VerificationRelated items
Showing items related by title and author.
-
Baarir, Souheib; Haddad, Serge; Ilié, Jean-Michel (2005) Communication / Conférence
-
Haddad, Serge; Ilié, Jean-Michel; Ajami, Khalil (2000) Communication / Conférence
-
Haddad, Serge; Ilié, Jean-Michel; Klai, Kais (2004) Communication / Conférence
-
Baarir, Souheib; Dutheillet, Claude; Haddad, Serge; Ilié, Jean-Michel (2005) Communication / Conférence
-
Klai, Kais; Haddad, Serge; Ilié, Jean-Michel (2005) Communication / Conférence