Document Open Access Logo

Reachability in Two-Parametric Timed Automata with One Parameter Is EXPSPACE-Complete

Authors Stefan Göller, Mathieu Hilaire

PDF
Thumbnail PDF

File

LIPIcs.STACS.2021.36.pdf
  • Filesize: 0.85 MB
  • 18 pages

Document Identifiers

Author Details

Stefan Göller
  • School of Electrical Engineering and Computer Science, Universität Kassel, Germany
Mathieu Hilaire
  • Université Paris-Saclay, ENS Paris-Saclay, Laboratoire Spécification et Vérification (LSV), CNRS, Gif-sur-Yvette, France

Funding

  • Göller, Stefan: The author was supported by the Agence Nationale de la Recherche grant no. ANR-17-CE40-0010.

Acknowledgements

We thank Benedikt Bollig and Karin Quaas for discussions and feedback.

Cite AsGet BibTex

Stefan Göller and Mathieu Hilaire. Reachability in Two-Parametric Timed Automata with One Parameter Is EXPSPACE-Complete. In 38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 187, pp. 36:1-36:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.STACS.2021.36

Abstract

Parametric timed automata (PTA) have been introduced by Alur, Henzinger, and Vardi as an extension of timed automata in which clocks can be compared against parameters. The reachability problem asks for the existence of an assignment of the parameters to the non-negative integers such that reachability holds in the underlying timed automaton. The reachability problem for PTA is long known to be undecidable, already over three parametric clocks. A few years ago, Bundala and Ouaknine proved that for PTA over two parametric clocks and one parameter the reachability problem is decidable and also showed a lower bound for the complexity class PSPACE^NEXP. Our main result is that the reachability problem for parametric timed automata over two parametric clocks and one parameter is EXPSPACE-complete. For the EXPSPACE lower bound we make use of deep results from complexity theory, namely a serializability characterization of EXPSPACE (in turn based on Barrington’s Theorem) and a logspace translation of numbers in Chinese Remainder Representation to binary representation due to Chiu, Davida, and Litow. It is shown that with small PTA over two parametric clocks and one parameter one can simulate serializability computations. For the EXPSPACE upper bound, we first give a careful exponential time reduction from PTA over two parametric clocks and one parameter to a (slight subclass of) parametric one-counter automata over one parameter based on a minor adjustment of a construction due to Bundala and Ouaknine. For solving the reachability problem for parametric one-counter automata with one parameter, we provide a series of techniques to partition a fictitious run into several carefully chosen subruns that allow us to prove that it is sufficient to consider a parameter value of exponential magnitude only. This allows us to show a doubly-exponential upper bound on the value of the only parameter of a PTA over two parametric clocks and one parameter. We hope that extensions of our techniques lead to finally establishing decidability of the long-standing open problem of reachability in parametric timed automata with two parametric clocks (and arbitrarily many parameters) and, if decidability holds, determining its precise computational complexity.

Subject Classification

ACM Subject Classification
  • Theory of computation → Timed and hybrid models
  • Theory of computation → Automata extensions
Keywords
  • Parametric Timed Automata
  • Computational Complexity
  • Reachability

Metrics

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

Related Versions

References

  1. Rajeev Alur, Costas Courcoubetis, and David L. Dill. Model-checking for real-time systems. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), Philadelphia, Pennsylvania, USA, June 4-7, 1990, pages 414-425. IEEE Computer Society, 1990. URL: https://doi.org/10.1109/LICS.1990.113766.
  2. Rajeev Alur and David L Dill. A theory of timed automata. Theoretical computer science, 126(2):183-235, 1994. Google Scholar
  3. Rajeev Alur, Thomas A Henzinger, and Moshe Y Vardi. Parametric real-time reasoning. In Proc. STOC'93, pages 592-601. ACM, 1993. Google Scholar
  4. Étienne André. What’s decidable about parametric timed automata? International Journal on Software Tools for Technology Transfer, 21(2):203-219, 2019. Google Scholar
  5. Étienne André. What’s decidable about parametric timed automata? Int. J. Softw. Tools Technol. Transf., 21(2):203-219, 2019. Google Scholar
  6. Sanjeev Arora and Boaz Barak. Computational Complexity: A Modern Approach. Cambrdige University Press, 2009. Google Scholar
  7. D. A. M. Barrington. Bounded-width polynomial-size branching programs recognize exactly those languages in NC¹. Journal of Computer and System Sciences, 38:150-164, 1989. Google Scholar
  8. Nikola Benes, Peter Bezdek, Kim Guldstrand Larsen, and Jirí Srba. Language emptiness of continuous-time parametric timed automata. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 69-81. Springer, 2015. Google Scholar
  9. Benedikt Bollig, Karin Quaas, and Arnaud Sangnier. The complexity of flat freeze ltl. Logical Methods in Computer Science, 15(3):32:1-32:26, 2019. URL: http://arxiv.org/abs/1609.06124.
  10. Daniel Bundala and Joel Ouaknine. On parametric timed automata and one-counter machines. Information and Computation, 253:272-303, 2017. Google Scholar
  11. Andrew Chiu, George Davida, and Bruce Litow. Division in logspace-uniform NC^1. Theoretical Informatics and Applications. Informatique Théorique et Applications, 35(3):259-275, 2001. Google Scholar
  12. Stéphane Demri and Arnaud Sangnier. When model-checking freeze LTL over counter machines becomes decidable. In C.-H. Luke Ong, editor, Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6014 of Lecture Notes in Computer Science, pages 176-190. Springer, 2010. Google Scholar
  13. Stefan Göller, Christoph Haase, Joël Ouaknine, and James Worrell. Model Checking Succinct and Parametric One-Counter Automata. In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul G. Spirakis, editors, Automata, Languages and Programming, 37th International Colloquium, ICALP 2010, Bordeaux, France, July 6-10, 2010, Proceedings, Part II, volume 6199 of Lecture Notes in Computer Science, pages 575-586. Springer, 2010. Google Scholar
  14. Stefan Göller and Mathieu Hilaire. Reachability in two-parametric timed automata with one parameter is EXPSPACE-complete. CoRR, abs/2011.07091, 2020. URL: http://arxiv.org/abs/2011.07091.
  15. Stefan Göller and Markus Lohrey. Branching-time model checking of one-counter processes and timed automata. SIAM J. Comput., 42(3):884-923, 2013. Google Scholar
  16. Christoph Haase. On the complexity of model checking counter automata. PhD thesis, Oxford University, 2012. Google Scholar
  17. Christoph Haase, Joël Ouaknine, and James Worrell. Relating reachability problems in timed and counter automata. Fundam. Informaticae, 143(3-4):317-338, 2016. Google Scholar
  18. Michael A. Harrison. Introduction to Formal Language Theory. Addison-Wesley, 1978. Google Scholar
  19. Thomas A. Henzinger, Zohar Manna, and Amir Pnueli. What good are digital clocks? In Werner Kuich, editor, Automata, Languages and Programming, 19th International Colloquium, ICALP92, Vienna, Austria, July 13-17, 1992, Proceedings, volume 623 of Lecture Notes in Computer Science, pages 545-558. Springer, 1992. Google Scholar
  20. Ulrich Hertrampf, Clemens Lautemann, Thomas Schwentick, Heribert Vollmer, and Klaus W. Wagner. On the power of polynomial time bit-reductions. In Proceedings of the Eighth Annual Structure in Complexity Theory Conference, pages 200-207. IEEE Computer Society Press, 1993. Google Scholar
  21. Antonia Lechner, Richard Mayr, Joël Ouaknine, Amaury Pouly, and James Worrell. Model checking flat freeze LTL on one-counter automata. Log. Methods Comput. Sci., 14(4), 2018. Google Scholar
  22. Joël Ouaknine and James Worrell. Universality and Language Inclusion for Open and Closed Timed Automata. In Oded Maler and Amir Pnueli, editors, Hybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3-5, 2003, Proceedings, volume 2623 of Lecture Notes in Computer Science, pages 375-388. Springer, 2003. URL: https://doi.org/10.1007/3-540-36580-X_28.
  23. C. H. Papadimitriou. Computational Complexity. Addison Wesley, 1994. 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