Journal article
Generalized discrete timed automata: decidable approximations for safety verification
Theoretical computer science, Vol.296(1), pp.59-74
2003
Handle:
https://hdl.handle.net/2376/113801
Abstract
We consider generalized discrete timed automata with general linear relations over clocks and parameterized constants as clock constraints and with parameterized durations. We look at three approximation techniques (i.e., the
r-reset-bounded approximation, the
B-bounded approximation, and the 〈
B,
r〉-crossing-bounded approximation), and derive automata-theoretic characterizations of the binary reachability under these approximations. The characterizations allow us to show that the safety analysis problem is decidable for generalized discrete timed automata with unit durations and for deterministic generalized discrete timed automata with parameterized durations. An example specification written in ASTRAL is used to run a number of experiments using one of the approximation techniques.
Metrics
9 Record Views
Details
- Title
- Generalized discrete timed automata: decidable approximations for safety verification
- Creators
- Zhe Dang - School of Electrical Engineering and Computer Science, Washington State University, Pullman, WA 99164, USAOscar H Ibarra - Department of Computer Science, University of California, Santa Barbara, CA 93106, USARichard A Kemmerer - Department of Computer Science, University of California, Santa Barbara, CA 93106, USA
- Publication Details
- Theoretical computer science, Vol.296(1), pp.59-74
- Academic Unit
- Electrical Engineering and Computer Science, School of
- Publisher
- Elsevier B.V
- Identifiers
- 99900547850401842
- Language
- English
- Resource Type
- Journal article