Anzeige
Erschienen in:
2005 | OriginalPaper | Buchkapitel
A New Modality for Almost Everywhere Properties in Timed Automata
verfasst von : Houda Bel Mokadem, Béatrice Bérard, Patricia Bouyer, François Laroussinie
Erschienen in: CONCUR 2005 – Concurrency Theory
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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
.