Document Open Access Logo

Timed Games and Deterministic Separability

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

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2020.121.pdf
  • Filesize: 0.6 MB
  • 16 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 ERC project Lipa (grant 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. We kindly thank the anonymous reviewers for their helpful comments.

Cite AsGet BibTex

Lorenzo Clemente, Sławomir Lasota, and Radosław Piórkowski. Timed Games and Deterministic Separability. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 121:1-121:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.ICALP.2020.121

Abstract

We study a generalisation of Büchi-Landweber games to the timed setting. The winning condition is specified by a non-deterministic timed automaton with epsilon transitions and only Player I can elapse time. We show that for fixed number of clocks and maximal numerical constant available to Player II, it is decidable whether she has a winning timed controller using these resources. More interestingly, we also show that the problem remains decidable even when the maximal numerical constant is not specified in advance, which is an important technical novelty not present in previous literature on timed games. We complement these two decidability result by showing undecidability when the number of clocks available to Player II is not fixed. As an application of timed games, and our main motivation to study them, we show that they can be used to solve the deterministic separability problem for nondeterministic timed automata with epsilon transitions. This is a novel decision problem about timed automata which has not been studied before. We show that separability is decidable when the number of clocks of the separating automaton is fixed and the maximal constant is not. The problem whether separability is decidable without bounding the number of clocks of the separator remains an interesting open problem.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Quantitative automata
  • Theory of computation → Timed and hybrid models
Keywords
  • Timed automata
  • separability problems
  • timed games

Metrics

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

Related Versions

References

  1. https://siglog.org/the-2016-alonzo-church-award-for-outstanding-contributions-to-logic-and-computation/, 2016. URL: https://siglog.org/the-2016-alonzo-church-award-for-outstanding-contributions-to-logic-and-computation/.
  2. 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.
  3. Rajeev Alur and David L. Dill. A theory of timed automata. Theor. Comput. Sci., 126:183-235, 1994. 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 SSSC'98, volume 31 (18) of 5th IFAC Conference on System Structure and Control, pages 447-452, 1998. URL: https://doi.org/10.1016/S1474-6670(17)42032-5.
  6. 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.
  7. Patricia Bouyer, Fabrice Chevalier, and Deepak D'Souza. Fault diagnosis using timed automata. In Proc. of FOSSACS'05, FOSSACS'05, pages 219-233, Berlin, Heidelberg, 2005. Springer-Verlag. URL: https://doi.org/10.1007/978-3-540-31982-5_14.
  8. 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, Proc. of ICALP'07, pages 825-837, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. Google Scholar
  9. J. Richard Büchi and Lawrence H. Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society, 138:295-311, 1969. URL: http://www.jstor.org/stable/1994916.
  10. 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
  11. Lorenzo Clemente, Wojciech Czerwiński, Sławomir Lasota, and Charles Paperman. Regular separability of parikh automata. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, Proc. of ICALP'17, volume 80, pages 117:1-117:13, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.117.
  12. Lorenzo Clemente, Wojciech Czerwinski, Slawomir Lasota, and Charles Paperman. Separability of Reachability Sets of Vector Addition Systems. In Proc. of STACS'17, volume 66 of LIPICs, pages 24:1-24:14, 2017. URL: https://doi.org/10.4230/LIPIcs.STACS.2017.24.
  13. Lorenzo Clemente, Sławomir Lasota, and Radosław Piórkowski. Timed games and deterministic separability. arXiv e-prints, page arXiv:2004.12868, April 2020. URL: http://arxiv.org/abs/2004.12868.
  14. Lorenzo Clemente, Paweł Parys, Sylvain Salvati, and Igor Walukiewicz. The diagonal problem for higher-order recursion schemes is decidable. In Proc. of LICS'16, 2016. URL: https://doi.org/10.1145/2933575.2934527.
  15. Hubert Comon and Yan Jurski. Timed automata and the theory of real numbers. In Proc. of CONCUR'99, CONCUR '99, pages 242-257, London, UK, UK, 1999. Springer-Verlag. Google Scholar
  16. Wojciech Czerwiński and Sławomir Lasota. Regular Separability of One Counter Automata. Logical Methods in Computer Science, Volume 15, Issue 2, June 2019. URL: https://lmcs.episciences.org/5563.
  17. Wojciech Czerwinski, Slawomir Lasota, Roland Meyer, Sebastian Muskalla, K. Narayan Kumar, and Prakash Saivasan. Regular Separability of Well-Structured Transition Systems. In Sven Schewe and Lijun Zhang, editors, 29th International Conference on Concurrency Theory (CONCUR 2018), volume 118 of Leibniz International Proceedings in Informatics (LIPIcs), pages 35:1-35:18, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.35.
  18. Wojciech Czerwiński, Wim Martens, and Tomáš Masopust. Efficient separability of regular languages by subsequences and suffixes. In Proc. of ICALP'14, ICALP'13, pages 150-161, Berlin, Heidelberg, 2013. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-39212-2_16.
  19. Wojciech Czerwiński, Wim Martens, Lorijn van Rooijen, and Marc Zeitoun. A note on decidable separability by piecewise testable languages. In Proc. of FCT'15, 2015. URL: https://doi.org/10.1007/978-3-319-22177-9_14.
  20. Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, and Mariëlle Stoelinga. The element of surprise in timed games. In Roberto Amadio and Denis Lugiez, editors, Proc. of CONCUR'03, pages 144-158, Berlin, Heidelberg, 2003. Springer Berlin Heidelberg. Google Scholar
  21. C. Dima. Computing reachability relations in timed automata. In Proc. of LICS'02, pages 177-186, 2002. Google Scholar
  22. Deepak D’souza and P. Madhusudan. Timed control synthesis for external specifications. In Helmut Alt and Afonso Ferreira, editors, Proc. of STACS'02, pages 571-582, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg. Google Scholar
  23. John Fearnley and Marcin Jurdzinski. Reachability in two-clock timed automata is PSPACE-complete. Inf. Comput., 243:26-36, 2015. Google Scholar
  24. Olivier Finkel. Undecidable problems about timed automata. In Proc. of FORMATS'06, FORMATS'06, pages 187-199, Berlin, Heidelberg, 2006. Springer-Verlag. URL: https://doi.org/10.1007/11867340_14.
  25. 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.
  26. 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.
  27. 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
  28. Jean Goubault-Larrecq and Sylvain Schmitz. Deciding Piecewise Testable Separability for Regular Tree Languages. In Proc. of ICALP'16, volume 55 of LIPIcs, pages 97:1-97:15, 2016. URL: https://doi.org/10.4230/LIPIcs.ICALP.2016.97.
  29. 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.
  30. Matthew Hague, Jonathan Kochems, and C.-H. Luke Ong. Unboundedness and downward closures of higher-order pushdown automata. In Proc. of POPL'16, POPL 2016, pages 151-163, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2837614.2837627.
  31. 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.
  32. H. B. Hunt, III. On the decidability of grammar problems. J. ACM, 29(2):429-447, April 1982. URL: https://doi.org/10.1145/322307.322317.
  33. Marcin Jurdziński and Ashutosh Trivedi. Reachability-time games on timed automata. In Proc. of ICALP'07, pages 838-849, Berlin, Heidelberg, 2007. Springer-Verlag. URL: http://dl.acm.org/citation.cfm?id=2394539.2394637.
  34. Eryk Kopczynski. Invisible pushdown languages. In Proc. of LICS'16, pages 867-872, 2016. URL: https://doi.org/10.1145/2933575.2933579.
  35. Pavel Krčál and Radek Pelánek. On sampled semantics of timed systems. In Sundar Sarukkai and Sandeep Sen, editors, Proc. of FSTTCS'05, volume 3821 of LNCS, pages 310-321. Springer, 2005. URL: https://doi.org/10.1007/11590156_25.
  36. 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
  37. 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.
  38. Oded Maler, Amir Pnueli, and Joseph Sifakis. On the synthesis of discrete controllers for timed systems. In Ernst W. Mayr and Claude Puech, editors, Proc. of STACS'95, pages 229-242, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg. Google Scholar
  39. 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.
  40. Thomas Place, Lorijn Rooijen, and Marc Zeitoun. Separating regular languages by piecewise testable and unambiguous languages. In Krishnendu Chatterjee and Jirí Sgall, editors, Proc. of MFCS'13, pages 729-740. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40313-2_64.
  41. Thomas Place, Lorijn van Rooijen, and Marc Zeitoun. Separating regular languages by locally testable and locally threshold testable languages. LMCS, 10(3), 2014. URL: https://doi.org/10.2168/LMCS-10(3:24)2014.
  42. Thomas Place and Marc Zeitoun. Going higher in the first-order quantifier alternation hierarchy on words. In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias, editors, Proc. of ICALP'14, pages 342-353, Berlin, Heidelberg, 2014. Springer. URL: https://doi.org/10.1007/978-3-662-43951-7_29.
  43. Thomas Place and Marc Zeitoun. Separating regular languages with first-order logic. Logical Methods in Computer Science, 12(1), 2016. URL: https://doi.org/10.2168/LMCS-12(1:5)2016.
  44. Michael O. Rabin. Weakly definable relations and special automata. In Yehoshua Bar-Hillel, editor, Mathematical Logic and Foundations of Set Theory, volume 59 of Studies in Logic and the Foundations of Mathematics, pages 1-23. Elsevier, 1970. URL: https://doi.org/10.1016/S0049-237X(08)71929-3.
  45. Thomas G. Szymanski and John H. Williams. Noncanonical extensions of bottom-up parsing techniques. SIAM Journal on Computing, 5(2):231-250, 1976. URL: https://doi.org/10.1137/0205019.
  46. 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
  47. Ramanathan S. Thinniyam and Georg Zetzsche. Regular Separability and Intersection Emptiness Are Independent Problems. In Arkadev Chattopadhyay and Paul Gastin, editors, Proc. of FSTTCS'19, volume 150 of Leibniz International Proceedings in Informatics (LIPIcs), pages 51:1-51:15, Dagstuhl, Germany, 2019. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2019.51.
  48. Stavros Tripakis. Folk theorems on the determinization and minimization of timed automata. Inf. Process. Lett., 99(6):222-226, September 2006. Google Scholar
  49. 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
  50. H. Wong-Toi and G. Hoffmann. The control of dense real-time discrete event systems. In Proc. of CDC'91, volume 2 of Proceedings of the 30th IEEE Conference on Decision and Control, pages 1527-1528, December 1991. URL: https://doi.org/10.1109/CDC.1991.261658.
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