A New Modality for Almost Everywhere Properties in Timed Automata
Bel Mokadem, Houda; Bérard, Béatrice; Bouyer, Patricia; Laroussinie, François (2005), A New Modality for Almost Everywhere Properties in Timed Automata, in Abadi, Martin; de Alfaro, Luca, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings, Springer : Berlin, p. 110-124. http://dx.doi.org/10.1007/11539452_12
TypeCommunication / Conférence
Conference title16th International Conference on Concurrency Theory (CONCUR 2005)
Conference citySan Francisco
Book title16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings
Book authorAbadi, Martin; de Alfaro, Luca
Series titleLecture Notes in Computer Science
Number of pages578
MetadataShow full item record
Abstract (EN)The context of this study is timed temporal logics for timed automata. In this paper, we propose an extension of the classical logic TCTL with a new Until modality, called “Until almost everywhere”. In the extended logic, it is possible, for instance, to express that a property is true at all positions of all runs, except on a negligible set of positions. Such properties are very convenient, for example in the framework of boolean program verification, where transitions result from changing variable values. We investigate the expressive power of this modality and in particular, we prove that it cannot be expressed with classical TCTL modalities. However, we show that model-checking the extended logic remains PSPACE-complete as for TCTL.
Subjects / KeywordsTCTL; timed automata
Showing items related by title and author.