Sciweavers

Share
STACS
2001
Springer

On Presburger Liveness of Discrete Timed Automata

11 years 9 months ago
On Presburger Liveness of Discrete Timed Automata
Using an automata-theoretic approach, we investigate the decidability of liveness properties (called Presburger liveness properties) for timed automata when Presburger formulas on configurations are allowed. While the general problem of checking a temporal logic such as TPTL augmented with Presburger clock constraints is undecidable, we show that there are various classes of Presburger liveness properties which are decidable for discrete timed automata. For instance, it is decidable, given a discrete timed automaton ¦ and a Presburger property § , whether there exists an ¨ -path of ¦ where § holds infinitely often. We also show that other classes of Presburger liveness properties are indeed undecidable for discrete timed automata, e.g., whether § holds infinitely often for each ¨ -path of ¦ . These results might give insights into the corresponding problems for timed automata over dense domains, and help in the definition of a fragment of linear temporal logic, augmented wi...
Zhe Dang, Pierluigi San Pietro, Richard A. Kemmere
Added 30 Jul 2010
Updated 30 Jul 2010
Type Conference
Year 2001
Where STACS
Authors Zhe Dang, Pierluigi San Pietro, Richard A. Kemmerer
Comments (0)
books