Timed temporal logics for abstracting transient states
Bel Mokadem, Houda; Bérard, Béatrice; Bouyer, Patricia; Laroussinie, François (2006), Timed temporal logics for abstracting transient states, in Graf, Susanne; Zhang, Wenhui, Automated Technology for Verification and Analysis. 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006, Proceedings, Springer : Berlin, p. 337-351. http://dx.doi.org/10.1007/11901914_26
TypeCommunication / Conférence
Conference title4th International Symposium on Automated Technology for Verification and Analysis (ATVA 2006)
Book titleAutomated Technology for Verification and Analysis. 4th International Symposium, ATVA 2006, Beijing, China, October 23-26, 2006, Proceedings
Book authorGraf, Susanne; Zhang, Wenhui
Series titleLecture Notes in Computer Science
Number of pages540
MetadataShow full item record
Abstract (EN)In previous work, the timed logic TCTL was extended with an “almost everywhere” Until modality which abstracts negligible sets of positions (i.e. with a null duration) along a run of a timed automaton. We propose here an extension of this logic with more powerful modalities, in order to specify properties abstracting transient states, which are events that last for less than k time units. Our main result is that model-checking is still decidable and PSPACE-complete for this extension. On the other hand, a second semantics is defined, in which we consider the total duration where the property does not hold along a run. In this case, we prove that model-checking is undecidable.
Subjects / Keywordsmodel-checking; TCTL
Showing items related by title and author.