Document Open Access Logo

History-Deterministic Timed Automata

Authors Thomas A. Henzinger, Karoliina Lehtinen, Patrick Totzke

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2022.14.pdf
  • Filesize: 0.68 MB
  • 21 pages

Document Identifiers

Author Details

Thomas A. Henzinger
  • IST Austria, Klosterneuburg, Austria
Karoliina Lehtinen
  • CNRS, Aix-Marseille University, University of Toulon, LIS, France
Patrick Totzke
  • University of Liverpool, UK

Funding

  • Henzinger, Thomas A.: This work was supported in part by the ERC-2020-AdG 101020093.
  • Totzke, Patrick: acknowledges support from the EPSRC, project no. EP/V025848/1.

Cite AsGet BibTex

Thomas A. Henzinger, Karoliina Lehtinen, and Patrick Totzke. History-Deterministic Timed Automata. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 14:1-14:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CONCUR.2022.14

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Timed Automata
  • History-determinism
  • Good-for-games
  • fair simulation
  • synthesis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Bader Abu Radi and Orna Kupferman. Minimizing gfg transition-based automata. In International Colloquium on Automata, Languages and Programming (ICALP). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2019. Google Scholar
  2. Shaull Almagor and Orna Kupferman. Good-enough synthesis. In Computer Aided Verification (CAV), volume 12225 of Lecture Notes in Computer Science, pages 541-563. Springer, 2020. Google Scholar
  3. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994. URL: https://doi.org/10.1016/0304-3975(94)90010-8.
  4. Rajeev Alur, Limor Fix, and Thomas A. Henzinger. Event-clock automata: A determinizable class of timed automata. Theoretical Computer Science, 211(1-2):253-273, 1999. URL: https://doi.org/10.1016/S0304-3975(97)00173-4.
  5. Rajeev Alur and Thomas A. Henzinger. Back to the future: Towards a theory of timed regular languages. In 33rd Annual Symposium on Foundations of Computer Science, pages 177-186. IEEE Computer Society, 1992. URL: https://doi.org/10.1109/SFCS.1992.267774.
  6. Marc Bagnol and Denis Kuperberg. Büchi Good-for-Games Automata Are Efficiently Recognizable. In Sumit Ganguly and Paritosh Pandya, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 122 of Leibniz International Proceedings in Informatics (LIPIcs), pages 16:1-16:14, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2018.16.
  7. Udi Boker, Denis Kuperberg, Karoliina Lehtinen, and Michal Skrzypczak. On succinctness and recognisability of alternating good-for-games automata. CoRR, abs/2002.07278, 2020. URL: http://arxiv.org/abs/2002.07278.
  8. Udi Boker and Karoliina Lehtinen. Good for games automata: From nondeterminism to alternation. In International Conference on Concurrency Theory (CONCUR), volume 140 of LIPIcs, pages 19:1-19:16, 2019. Google Scholar
  9. Udi Boker and Karoliina Lehtinen. History Determinism vs. Good for Gameness in Quantitative Automata. In Mikołaj Bojańczy and Chandra Chekuri, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 213 of Leibniz International Proceedings in Informatics (LIPIcs), pages 38:1-38:20, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2021.38.
  10. Udi Boker and Karoliina Lehtinen. Token games and history-deterministic quantitative automata. In Patricia Bouyer and Lutz Schröder, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), pages 120-139, Cham, 2022. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-99253-8_7.
  11. Krishnendu Chatterjee, Thomas A. Henzinger, and Vinayak S. Prabhu. Timed parity games: Complexity and robustness. In Franck Cassez and Claude Jard, editors, International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), pages 124-140, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. Google Scholar
  12. Thomas Colcombet. The theory of stabilisation monoids and regular cost functions. In International Colloquium on Automata, Languages and Programming (ICALP), pages 139-150, 2009. Google Scholar
  13. Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, and Mariëlle Stoelinga. The element of surprise in timed games. In International Conference on Concurrency Theory (CONCUR), volume 2761 of Lecture Notes in Computer Science, pages 142-156. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45187-7_9.
  14. Deepak D’souza and P. Madhusudan. Timed control synthesis for external specifications. In International Symposium on Theoretical Aspects of Computer Science (STACS), pages 571-582. Springer Berlin Heidelberg, 2002. URL: https://doi.org/10.1007/3-540-45841-7_47.
  15. Emmanuel Filiot, Christof Löding, and Sarah Winter. Synthesis from weighted specifications with partial domains over finite words. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2020. Google Scholar
  16. Olivier Finkel. Undecidable problems about timed automata. In International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), volume 4202 of Lecture Notes in Computer Science, pages 187-199. Springer, 2006. URL: https://doi.org/10.1007/11867340_14.
  17. Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. A Bit of Nondeterminism Makes Pushdown Automata Expressive and Succinct. In Filippo Bonchi and Simon J. Puglisi, editors, International Symposium on Mathematical Foundations of Computer Science (MFCS), volume 202 of Leibniz International Proceedings in Informatics (LIPIcs), pages 53:1-53:20, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.MFCS.2021.53.
  18. T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. In ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 394-406, 1992. URL: https://doi.org/10.1109/LICS.1992.185551.
  19. Thomas A. Henzinger, Peter W. Kopke, and Howard Wong-Toi. The expressive power of clocks. In International Colloquium on Automata, Languages and Programming (ICALP), volume 944 of Lecture Notes in Computer Science, pages 417-428. Springer, 1995. URL: https://doi.org/10.1007/3-540-60084-1_93.
  20. Thomas A. Henzinger, Orna Kupferman, and Sriram K. Rajamani. Fair simulation. In International Conference on Concurrency Theory (CONCUR), pages 273-287. Springer Berlin Heidelberg, 1997. Google Scholar
  21. Thomas A. Henzinger and Nir Piterman. Solving games without determinization. In Zoltán Ésik, editor, Computer Science Logic (CSL), pages 395-410, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  22. Marcin Jurdzinski, Francois Laroussinie, and Jeremy Sproston. Model Checking Probabilistic Timed Automata with One or Two Clocks. Logical Methods in Computer Science, Volume 4, Issue 3, September 2008. URL: https://doi.org/10.2168/LMCS-4(3:12)2008.
  23. Denis Kuperberg and Michał Skrzypczak. On determinisation of good-for-games automata. In International Colloquium on Automata, Languages and Programming (ICALP), pages 299-310, 2015. Google Scholar
  24. Orna Kupferman, Shmuel Safra, and Moshe Y Vardi. Relating word and tree automata. Ann. Pure Appl. Logic, 138(1-3):126-146, 2006. Conference version in 1996. Google Scholar
  25. Karoliina Lehtinen and Martin Zimmermann. Good-for-games ω-pushdown automata. Logical Methods in Computer Science, 18, 2022. Google Scholar
  26. Donald A Martin. Borel determinacy. Annals of Mathematics, 102(2):363-371, 1975. Google Scholar
  27. Sven Schewe. Minimising good-for-games automata is np-complete. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2020. Google Scholar
  28. Serdar Tasiran, Rajeev Alur, Robert P. Kurshan, and Robert K. Brayton. Verifying abstractions of timed systems. In International Conference on Concurrency Theory (CONCUR), volume 1119 of Lecture Notes in Computer Science, pages 546-562. Springer, 1996. URL: https://doi.org/10.1007/3-540-61604-7_75.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact