Document Open Access Logo

Determinisability of One-Clock Timed Automata

Authors Lorenzo Clemente , Sławomir Lasota , Radosław Piórkowski

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.42.pdf
  • Filesize: 0.65 MB
  • 17 pages

Document Identifiers

Author Details

Lorenzo Clemente
  • University of Warsaw, Poland
Sławomir Lasota
  • University of Warsaw, Poland
Radosław Piórkowski
  • University of Warsaw, Poland

Funding

  • Clemente, Lorenzo: Partially supported by the Polish NCN grant 2017/26/D/ST6/00201.
  • Lasota, Sławomir: Partially supported by the Polish NCN grant 2019/35/B/ST6/02322 and by the ERC grant LIPA, agreement no. 683080.
  • Piórkowski, Radosław: Partially supported by the Polish NCN grant 2017/27/B/ST6/02093.

Acknowledgements

We thank S. Krishna for fruitful discussions and the anonymous reviewers for their constructive comments.

Cite AsGet BibTex

Lorenzo Clemente, Sławomir Lasota, and Radosław Piórkowski. Determinisability of One-Clock Timed Automata. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 42:1-42:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CONCUR.2020.42

Abstract

The deterministic membership problem for timed automata asks whether the timed language recognised by a nondeterministic timed automaton can be recognised by a deterministic timed automaton. We show that the problem is decidable when the input automaton is a one-clock nondeterministic timed automaton without epsilon transitions and the number of clocks of the deterministic timed automaton is fixed. We show that the problem in all the other cases is undecidable, i.e., when either 1) the input nondeterministic timed automaton has two clocks or more, or 2) it uses epsilon transitions, or 3) the number of clocks of the output deterministic automaton is not fixed.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Timed and hybrid models
Keywords
  • Timed automata
  • determinisation
  • deterministic membership problem

Metrics

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

Related Versions

References

  1. S. Akshay, Paul Gastin, and Shankara Narayanan Krishna. Analyzing Timed Systems Using Tree Automata. Logical Methods in Computer Science, Volume 14, Issue 2, May 2018. URL: https://doi.org/10.23638/LMCS-14(2:8)2018.
  2. Rajeev Alur and David L. Dill. A theory of timed automata. Theor. Comput. Sci., 126:183-235, 1994. Google Scholar
  3. Rajeev Alur, Limor Fix, and Thomas A. Henzinger. Event-clock automata: a determinizable class of timed automata. Theor. Comput. Sci., 211:253-273, January 1999. Google Scholar
  4. Eugene Asarin and Oded Maler. As soon as possible: Time optimal control for timed automata. In Proc. of HSCC'99, HSCC '99, pages 19-30, London, UK, UK, 1999. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=646879.710314.
  5. Eugene Asarin, Oded Maler, Amir Pnueli, and Joseph Sifakis. Controller synthesis for timed automata. In Proc. of the 5th IFAC Conference on System Structure and Control (SSSC'98), volume 31 (18), pages 447-452, 1998. URL: https://doi.org/10.1016/S1474-6670(17)42032-5.
  6. Christel Baier, Nathalie Bertrand, Patricia Bouyer, and Thomas Brihaye. When are timed automata determinizable? In Susanne Albers, Alberto Marchetti-Spaccamela, Yossi Matias, Sotiris Nikoletseas, and Wolfgang Thomas, editors, Proc of ICALP'09, pages 43-54, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. Google Scholar
  7. Vince Bárány, Christof Löding, and Olivier Serre. Regularity problems for visibly pushdown languages. In Proc. of STACS'06, STACS'06, pages 420-431, Berlin, Heidelberg, 2006. Springer-Verlag. URL: https://doi.org/10.1007/11672142_34.
  8. Gerd Behrmann, Alexandre David, Kim G. Larsen, John Hakansson, Paul Petterson, Wang Yi, and Martijn Hendriks. Uppaal 4.0. In Proceedings of the 3rd International Conference on the Quantitative Evaluation of Systems, QEST '06, pages 125-126, Washington, DC, USA, 2006. IEEE Computer Society. URL: https://doi.org/10.1109/QEST.2006.59.
  9. Nathalie Bertrand, Amélie Stainer, Thierry Jéron, and Moez Krichen. A game approach to determinize timed automata. Formal Methods in System Design, 46(1):42-80, 2015. URL: https://doi.org/10.1007/s10703-014-0220-1.
  10. Mikolaj Bojańczyk and Sławomir Lasota. A machine-independent characterization of timed languages. In Proc. ICALP 2012, pages 92-103, 2012. Google Scholar
  11. Patricia Bouyer, Fabrice Chevalier, and Deepak D'Souza. Fault diagnosis using timed automata. In Proc. of FOSSACS'05, pages 219-233, Berlin, Heidelberg, 2005. Springer-Verlag. URL: https://doi.org/10.1007/978-3-540-31982-5_14.
  12. Thomas Brihaye, Thomas A. Henzinger, Vinayak S. Prabhu, and Jean-François Raskin. Minimum-time reachability in timed games. In Lars Arge, Christian Cachin, Tomasz Jurdziński, and Andrzej Tarlecki, editors, In Proc. of ICALP'07, pages 825-837, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. Google Scholar
  13. Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. On the expressiveness of Parikh automata and related models. In Rudolf Freund, Markus Holzer, Carlo Mereghetti, Friedrich Otto, and Beatrice Palano, editors, Proc. of NCMA'11, volume 282 of books@ocg.at, pages 103-119. Austrian Computer Society, 2011. Google Scholar
  14. Franck Cassez, Alexandre David, Emmanuel Fleury, Kim G. Larsen, and Didier Lime. Efficient on-the-fly algorithms for the analysis of timed games. In Martín Abadi and Luca de Alfaro, editors, Proc. of CONCUR'05, pages 66-80, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  15. Pierre Chambart and Philippe Schnoebelen. The ordinal recursive complexity of lossy channel systems. In Proc. of LICS'08, pages 205-216, 2008. Google Scholar
  16. Lorenzo Clemente, Piotr Hofman, and Patrick Totzke. Timed Basic Parallel Processes. In Wan Fokkink and Rob van Glabbeek, editors, Proc. of CONCUR'19, volume 140 of Leibniz International Proceedings in Informatics (LIPIcs), pages 15:1-15:16, Dagstuhl, Germany, 2019. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.15.
  17. Lorenzo Clemente, Sławomir Lasota, and Radosław Piórkowski. Determinisability of one-clock timed automata. arXiv e-prints, July 2020. URL: http://arxiv.org/abs/2007.09340.
  18. Lorenzo Clemente, Sławomir Lasota, and Radosław Piórkowski. Timed games and deterministic separability. In Proc. of ICALP 2020, pages 121:1-121:16, 2020. Google Scholar
  19. Hubert Comon and Yan Jurski. Timed automata and the theory of real numbers. In Proc. of CONCUR'99, pages 242-257, London, UK, UK, 1999. Springer-Verlag. Google Scholar
  20. C. Dima. Computing reachability relations in timed automata. In Proc. of LICS'02, pages 177-186, 2002. Google Scholar
  21. John Fearnley and Marcin Jurdziński. Reachability in two-clock timed automata is PSPACE-complete. Information and Computation, 243:26-36, 2015. URL: https://doi.org/10.1016/j.ic.2014.12.004.
  22. Olivier Finkel. Undecidable problems about timed automata. In Proc. of FORMATS'06, pages 187-199, Berlin, Heidelberg, 2006. Springer-Verlag. URL: https://doi.org/10.1007/11867340_14.
  23. Martin Fränzle, Karin Quaas, Mahsa Shirmohammadi, and James Worrell. Effective definability of the reachability relation in timed automata. Information Processing Letters, 153:105871, 2020. URL: https://doi.org/10.1016/j.ipl.2019.105871.
  24. Laurent Fribourg. A closed-form evaluation for extended timed automata. Technical report, CNRS & ECOLE NORMALE SUPERIEURE DE CACHAN, 1998. Google Scholar
  25. Paul Gastin, Sayan Mukherjee, and B. Srivathsan. Reachability in Timed Automata with Diagonal Constraints. In Sven Schewe and Lijun Zhang, editors, Proc. of CONCUR'18, volume 118 of Leibniz International Proceedings in Informatics (LIPIcs), pages 28:1-28:17, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.28.
  26. Paul Gastin, Sayan Mukherjee, and B. Srivathsan. Fast algorithms for handling diagonal constraints in timed automata. In Isil Dillig and Serdar Tasiran, editors, Computer Aided Verification, pages 41-59, Cham, 2019. Springer International Publishing. Google Scholar
  27. Stefan Göller and Paweł Parys. Bisimulation finiteness of pushdown systems is elementary. In Proc. of LICS'20, pages 521-534, 2020. Google Scholar
  28. R. Govind, Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Revisiting Local Time Semantics for Networks of Timed Automata. In Wan Fokkink and Rob van Glabbeek, editors, Proc. of CONCUR 2019, volume 140 of Leibniz International Proceedings in Informatics (LIPIcs), pages 16:1-16:15, Dagstuhl, Germany, 2019. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2019.16.
  29. Frédéric Herbreteau, B. Srivathsan, and Igor Walukiewicz. Better abstractions for timed automata. Information and Computation, 251:67-90, 2016. URL: https://doi.org/10.1016/j.ic.2016.07.004.
  30. Marcin Jurdziński and Ashutosh Trivedi. Reachability-time games on timed automata. In In Proc. of ICALP'07, pages 838-849, Berlin, Heidelberg, 2007. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=2394539.2394637.
  31. Pavel Krčál and Radek Pelánek. On sampled semantics of timed systems. In Sundar Sarukkai and Sandeep Sen, editors, In Proc. of FSTTCS'05, volume 3821 of LNCS, pages 310-321. Springer, 2005. URL: https://doi.org/10.1007/11590156_25.
  32. M. Kwiatkowska, G. Norman, and D. Parker. PRISM 4.0: Verification of probabilistic real-time systems. In G. Gopalakrishnan and S. Qadeer, editors, Proc. of CAV'11, volume 6806 of LNCS, pages 585-591. Springer, 2011. Google Scholar
  33. Slawomir Lasota and Igor Walukiewicz. Alternating timed automata. ACM Trans. Comput. Logic, 9(2):10:1-10:27, 2008. URL: https://doi.org/10.1145/1342991.1342994.
  34. Oded Maler and Amir Pnueli. On recognizable timed languages. In Igor Walukiewicz, editor, Proc. of FOSSACS'04, volume 2987 of LNCS, pages 348-362. Springer Berlin Heidelberg, 2004. URL: https://doi.org/10.1007/978-3-540-24727-2_25.
  35. Richard Mayr. Undecidable problems in unreliable computations. Theor. Comput. Sci., 297(1-3):337-354, March 2003. URL: https://doi.org/10.1016/S0304-3975(02)00646-1.
  36. Brian Nielsen and Arne Skou. Automated test generation from timed automata. International Journal on Software Tools for Technology Transfer, 5(1):59-77, November 2003. URL: https://doi.org/10.1007/s10009-002-0094-1.
  37. Joël Ouaknine and James Worrell. On the language inclusion problem for timed automata: Closing a decidability gap. In Proc. of LICS'04, pages 54-63, 2004. URL: https://doi.org/10.1109/LICS.2004.1319600.
  38. Joel Ouaknine and James Worrell. On the decidability and complexity of Metric Temporal Logic over finite words. Logical Methods in Computer Science, Volume 3, Issue 1, February 2007. URL: https://doi.org/10.2168/LMCS-3(1:8)2007.
  39. Jeffrey Shallit. A Second Course in Formal Languages and Automata Theory. Cambridge University Press, 2008. URL: https://doi.org/10.1017/CBO9780511808876.
  40. P. Vijay Suman, Paritosh K. Pandya, Shankara Narayanan Krishna, and Lakshmi Manasa. Timed automata with integer resets: Language inclusion and expressiveness. In Proc. of FORMATS'08, pages 78-92, Berlin, Heidelberg, 2008. Springer-Verlag. URL: https://doi.org/10.1007/978-3-540-85778-5_7.
  41. Martin Tappler, Bernhard K. Aichernig, Kim Guldstrand Larsen, and Florian Lorber. Time to learn - learning timed automata from tests. In Étienne André and Mariëlle Stoelinga, editors, Proc. of FORMATS'19, pages 216-235, Cham, 2019. Springer International Publishing. Google Scholar
  42. Stavros Tripakis. Folk theorems on the determinization and minimization of timed automata. Inf. Process. Lett., 99(6):222-226, September 2006. Google Scholar
  43. Leslie G. Valiant. Regularity and related problems for deterministic pushdown automata. J. ACM, 22(1):1-10, January 1975. URL: https://doi.org/10.1145/321864.321865.
  44. Rüdiger Valk and Guy Vidal-Naquet. Petri nets and regular languages. Journal of Computer and System Sciences, 23(3):299-325, 1981. URL: https://doi.org/10.1016/0022-0000(81)90067-2.
  45. Sicco Verwer, Mathijs de Weerdt, and Cees Witteveen. An algorithm for learning real-time automata. In Proc of. the Annual Belgian-Dutch Machine Learning Conference (Benelearn'078), 2007. Google Scholar
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