Conference item
Revisiting reachability in timed automata
- Abstract:
- We revisit a fundamental result in real-time verification, namely that the binary reachability relation between configurations of a given timed automaton is definable in linear arithmetic over the integers and reals. In this paper we give a new and simpler proof of this result, building on the well-known reachability analysis of timed automata involving difference bound matrices. Using this new proof, we give an exponential-space procedure for model checking the reachability fragment of the logic parametric TCTL. Finally we show that the latter problem is NEXPTIME-hard.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Access Document
- Files:
-
-
(Preview, Accepted manuscript, pdf, 384.4KB, Terms of use)
-
- Publisher copy:
- 10.1109/LICS.2017.8005098
Authors
- Publisher:
- Institute of Electrical and Electronics Engineers
- Host title:
- Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)
- Journal:
- Thirty-Second Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017) More from this journal
- Publication date:
- 2017-08-18
- Acceptance date:
- 2017-03-21
- DOI:
- ISSN:
-
1043-6871
- Keywords:
- Pubs id:
-
pubs:681755
- UUID:
-
uuid:c761bf36-6ced-4ffa-91b7-a4bc146c4c97
- Local pid:
-
pubs:681755
- Source identifiers:
-
681755
- Deposit date:
-
2018-09-05
- ARK identifier:
Terms of use
- Copyright holder:
- Institute of Electrical and Electronics Engineers
- Copyright date:
- 2017
- Notes:
- ©2017 IEEE This is the accepted manuscript version of the article. The final version is available online from Institute of Electrical and Electronics Engineers at: https://doi.org/10.1109/LICS.2017.8005098
If you are the owner of this record, you can report an update to it here: Report update to this record