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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Bel Mokadem, H., Bérard, B., Bouyer, P., & Laroussinie, F. (2005). A new modality for almost everywhere properties in timed automata. In Lecture Notes in Computer Science (Vol. 3653, pp. 110–124). Springer Verlag. https://doi.org/10.1007/11539452_12
Mendeley helps you to discover research relevant for your work.