Show simple item record

dc.contributor.authorAjami, Khalil
dc.contributor.authorHaddad, Serge
HAL ID: 745039
dc.contributor.authorIlié, Jean-Michel
dc.date.accessioned2010-11-16T13:33:39Z
dc.date.available2010-11-16T13:33:39Z
dc.date.issued1998
dc.identifier.urihttps://basepub.dauphine.fr/handle/123456789/5085
dc.language.isoenen
dc.subjectLTLen
dc.subjectTemporal Logicen
dc.subjectSymmetriesen
dc.subjectBüchi automataen
dc.subjectModel Checkingen
dc.subjectVerificationen
dc.subject.ddc004en
dc.titleExploiting Symmetry in Linear Time Temporal Logic Model Checking : One Step Beyonden
dc.typeCommunication / Conférence
dc.description.abstractenModel 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.en
dc.identifier.citationpages52-67en
dc.relation.ispartofseriestitleLecture Notes in Computer Science
dc.relation.ispartofseriesnumber1384
dc.relation.ispartoftitleTools 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, Proceedingsen
dc.relation.ispartofeditorSteffen, Bernhard
dc.relation.ispartofpublnameSpringeren
dc.relation.ispartofpublcityBerlinen
dc.relation.ispartofdate1998
dc.relation.ispartofpages457en
dc.relation.ispartofurlhttp://dx.doi.org/10.1007/BFb0054159en
dc.description.sponsorshipprivateouien
dc.subject.ddclabelInformatique généraleen
dc.relation.ispartofisbn978-3-540-64356-2en
dc.relation.conftitle4th International Conference on Tools and Algorithms for the construction and Analysis of Systems (TACAS'98)en
dc.relation.confdate1998-03
dc.relation.confcityLisbonneen
dc.relation.confcountryPortugalen
dc.identifier.doihttp://dx.doi.org/10.1007/BFb0054164


Files in this item

FilesSizeFormatView

There are no files associated with this item.

This item appears in the following Collection(s)

Show simple item record