Journal article
Presburger liveness verification of discrete timed automata
Theoretical computer science, Vol.299(1-3), pp.413-438
04/18/2003
Handle:
https://hdl.handle.net/2376/115568
Abstract
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 A and a Presburger property P, whether there exists an ω-path of A where P holds infinitely often. We also show that other classes of Presburger liveness properties are indeed undecidable for discrete timed automata, e.g., whether P holds infinitely often for eachω-path of A. 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 with Presburger conditions on configurations, which is decidable for model checking timed automata.
Metrics
12 Record Views
Details
- Title
- Presburger liveness verification of discrete timed automata
- Creators
- Zhe Dang - School of Electrical Engineering and Computer Science, Washington State University, Pullman, WA 99164, USAPierluigi San Pietro - Dipartimento di Elettronica e Informazione, Politecnico di Milano, ItalyRichard A Kemmerer - Department of Computer Science, University of California at Santa Barbara, CA 93106, USA
- Publication Details
- Theoretical computer science, Vol.299(1-3), pp.413-438
- Academic Unit
- Electrical Engineering and Computer Science, School of
- Publisher
- Elsevier B.V
- Identifiers
- 99900548482101842
- Language
- English
- Resource Type
- Journal article