History-deterministic timed automata
Henzinger TA, Lehtinen K, Totzke P. 2022. History-deterministic timed automata. 33rd International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 243, 14:1-14:21.
Download
Conference Paper
| Published
| English
Scopus indexed
Author
Henzinger, Thomas AISTA ;
Lehtinen, Karoliina;
Totzke, Patrick
Department
Series Title
LIPIcs
Abstract
We explore the notion of history-determinism in the context of timed automata (TA). History-deterministic automata are those in which nondeterminism can be resolved on the fly, based on the run constructed thus far. History-determinism is a robust property that admits different game-based characterisations, and history-deterministic specifications allow for game-based verification without an expensive determinization step.
We show yet another characterisation of history-determinism in terms of fair simulation, at the general level of labelled transition systems: a system is history-deterministic precisely if and only if it fairly simulates all language smaller systems.
For timed automata over infinite timed words it is known that universality is undecidable for Büchi TA. We show that for history-deterministic TA with arbitrary parity acceptance, timed universality, inclusion, and synthesis all remain decidable and are ExpTime-complete.
For the subclass of TA with safety or reachability acceptance, we show that checking whether such an automaton is history-deterministic is decidable (in ExpTime), and history-deterministic TA with safety acceptance are effectively determinizable without introducing new automata states.
Publishing Year
Date Published
2022-09-06
Proceedings Title
33rd International Conference on Concurrency Theory
Publisher
Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Acknowledgement
Thomas A. Henzinger: This work was supported in part by the ERC-2020-AdG 101020093.
Patrick Totzke: acknowledges support from the EPSRC, project no. EP/V025848/1.
Volume
243
Page
14:1-14:21
Conference
CONCUR: Conference on Concurrency Theory
Conference Location
Warsaw, Poland
Conference Date
2022-09-13 – 2022-09-16
ISBN
ISSN
IST-REx-ID
Cite this
Henzinger TA, Lehtinen K, Totzke P. History-deterministic timed automata. In: 33rd International Conference on Concurrency Theory. Vol 243. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2022:14:1-14:21. doi:10.4230/LIPIcs.CONCUR.2022.14
Henzinger, T. A., Lehtinen, K., & Totzke, P. (2022). History-deterministic timed automata. In 33rd International Conference on Concurrency Theory (Vol. 243, p. 14:1-14:21). Warsaw, Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CONCUR.2022.14
Henzinger, Thomas A, Karoliina Lehtinen, and Patrick Totzke. “History-Deterministic Timed Automata.” In 33rd International Conference on Concurrency Theory, 243:14:1-14:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. https://doi.org/10.4230/LIPIcs.CONCUR.2022.14.
T. A. Henzinger, K. Lehtinen, and P. Totzke, “History-deterministic timed automata,” in 33rd International Conference on Concurrency Theory, Warsaw, Poland, 2022, vol. 243, p. 14:1-14:21.
Henzinger TA, Lehtinen K, Totzke P. 2022. History-deterministic timed automata. 33rd International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 243, 14:1-14:21.
Henzinger, Thomas A., et al. “History-Deterministic Timed Automata.” 33rd International Conference on Concurrency Theory, vol. 243, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022, p. 14:1-14:21, doi:10.4230/LIPIcs.CONCUR.2022.14.
All files available under the following license(s):
Creative Commons Attribution 4.0 International Public License (CC-BY 4.0):
Main File(s)
File Name
2022_LIPICs_Henzinger2.pdf
717.94 KB
Access Level
Open Access
Date Uploaded
2023-02-06
MD5 Checksum
9e97e15628f66b2ad77f535bb0327dee