• xmlui.mirage2.page-structure.header.title
    • français
    • English
  • Help
  • Login
  • Language 
    • Français
    • English
View Item 
  •   BIRD Home
  • LAMSADE (UMR CNRS 7243)
  • LAMSADE : Publications
  • View Item
  •   BIRD Home
  • LAMSADE (UMR CNRS 7243)
  • LAMSADE : Publications
  • View Item
JavaScript is disabled for your browser. Some features of this site may not work without it.

Browse

BIRDResearch centres & CollectionsBy Issue DateAuthorsTitlesTypeThis CollectionBy Issue DateAuthorsTitlesType

My Account

LoginRegister

Statistics

Most Popular ItemsStatistics by CountryMost Popular Authors
Thumbnail - Request a copy

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érence
Date
1998
Conference title
4th International Conference on Tools and Algorithms for the construction and Analysis of Systems (TACAS'98)
Conference date
1998-03
Conference city
Lisbonne
Conference country
Portugal
Book 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, Proceedings
Book author
Steffen, Bernhard
Publisher
Springer
Series title
Lecture Notes in Computer Science
Series number
1384
Published in
Berlin
ISBN
978-3-540-64356-2
Number of pages
457
Pages
52-67
Publication identifier
http://dx.doi.org/10.1007/BFb0054164
Metadata
Show full item record
Author(s)
Ajami, Khalil
Haddad, Serge
Ilié, Jean-Michel
Abstract (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; Verification

Related items

Showing items related by title and author.

  • Thumbnail
    Exploiting Partial Symmetries in Well-formed nets for the Reachability and the Linear Time Model Checking Problems 
    Baarir, Souheib; Haddad, Serge; Ilié, Jean-Michel (2005) Communication / Conférence
  • Thumbnail
    A Model Checking Method for Partially Symmetric Systems 
    Haddad, Serge; Ilié, Jean-Michel; Ajami, Khalil (2000) Communication / Conférence
  • Thumbnail
    Design and Evaluation of a Symbolic and Abstraction-Based Model Checker 
    Haddad, Serge; Ilié, Jean-Michel; Klai, Kais (2004) Communication / Conférence
  • Thumbnail
    On the use of exact lumpability in partially symmetrical Well-formed Nets 
    Baarir, Souheib; Dutheillet, Claude; Haddad, Serge; Ilié, Jean-Michel (2005) Communication / Conférence
  • Thumbnail
    Modular Verification of Petri nets properties: a Structure-based Approach 
    Klai, Kais; Haddad, Serge; Ilié, Jean-Michel (2005) Communication / Conférence
Dauphine PSL Bibliothèque logo
Place du Maréchal de Lattre de Tassigny 75775 Paris Cedex 16
Phone: 01 44 05 40 94
Contact
Dauphine PSL logoEQUIS logoCreative Commons logo