Sciweavers

CONCUR
2005
Springer

A New Modality for Almost Everywhere Properties in Timed Automata

13 years 11 months ago
A New Modality for Almost Everywhere Properties in Timed Automata
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.
Houda Bel Mokadem, Béatrice Bérard,
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where CONCUR
Authors Houda Bel Mokadem, Béatrice Bérard, Patricia Bouyer, François Laroussinie
Comments (0)