Document Open Access Logo

Binary Reachability of Timed Pushdown Automata via Quantifier Elimination and Cyclic Order Atoms

Authors Lorenzo Clemente , Slawomir Lasota

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2018.118.pdf
  • Filesize: 0.53 MB
  • 14 pages

Document Identifiers

Author Details

Lorenzo Clemente
  • University of Warsaw
Slawomir Lasota
  • University of Warsaw

Funding

  • Clemente, Lorenzo: Partially supported by Polish NCN grant 2017/26/D/ST6/00201.
  • Lasota, Slawomir: Partially supported by Polish NCN grant 2016/21/B/ST6/01505.

Cite As Get BibTex

Lorenzo Clemente and Slawomir Lasota. Binary Reachability of Timed Pushdown Automata via Quantifier Elimination and Cyclic Order Atoms. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 118:1-118:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.ICALP.2018.118

Abstract

We study an expressive model of timed pushdown automata extended with modular and fractional clock constraints. We show that the binary reachability relation is effectively expressible in hybrid linear arithmetic with a rational and an integer sort. This subsumes analogous expressibility results previously known for finite and pushdown timed automata with untimed stack. As key technical tools, we use quantifier elimination for a fragment of hybrid linear arithmetic and for cyclic order atoms, and a reduction to register pushdown automata over cyclic order atoms.

Subject Classification

ACM Subject Classification
  • Theory of computation → Timed and hybrid models
  • Theory of computation → Logic and verification
  • Theory of computation → Formal languages and automata theory
Keywords
  • timed automata
  • reachability relation
  • timed pushdown automata
  • linear arithmetic

Metrics

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

References

  1. P. A. Abdulla, M. F. Atig, and J. Stenman. Dense-timed pushdown automata. In Proc. LICS'12, pages 35-44. IEEE, 2012. URL: http://dx.doi.org/10.1109/LICS.2012.15.
  2. Rajeev Alur and David L. Dill. A theory of timed automata. Theor. Comput. Sci., 126:183-235, 1994. Google Scholar
  3. M. Benerecetti, S. Minopoli, and A. Peron. Analysis of timed recursive state machines. In Proc. TIME'10, pages 61-68. IEEE, sept. 2010. URL: http://dx.doi.org/10.1109/TIME.2010.10.
  4. Mikołaj Bojańczyk. Slightly infinite sets. URL: https://www.mimuw.edu.pl/~bojan/paper/atom-book.
  5. Ahmed Bouajjani, Rachid Echahed, and Riadh Robbana. On the automatic verification of systems with continuous variables and unbounded discrete data structures. In Proc. Hybrid Systems '94, volume 999 of LNCS, pages 64-85. Springer, 1995. Google Scholar
  6. Lorenzo Clemente. Decidability of timed communicating automata. ArXiv e-prints, 04 2018. URL: http://arxiv.org/abs/1804.07815.
  7. Lorenzo Clemente and Slawomir Lasota. Reachability analysis of first-order definable pushdown systems. In Proc. of CSL'15, volume 41 of LIPIcs, pages 244-259. Dagstuhl, 2015. Google Scholar
  8. Lorenzo Clemente and Slawomir Lasota. Timed pushdown automata revisited. In Proc. LICS'15, pages 738-749. IEEE, July 2015. Google Scholar
  9. Lorenzo Clemente, Sławomir Lasota, Ranko Lazić, and Filip Mazowiecki. Timed pushdown automata and branching vector addition systems. In Proc. of LICS'17, 2017. Google Scholar
  10. Lorenzo Clemente and Sławomir Lasota. Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms. ArXiv e-prints, 04 2018. URL: http://arxiv.org/abs/1804.10772.
  11. 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
  12. Zhe Dang. Pushdown timed automata: a binary reachability characterization and safety verification. Theor. Comput. Sci., 302(1-3):93-121, 2003. URL: http://dx.doi.org/10.1016/S0304-3975(02)00743-0.
  13. C. Dima. Computing reachability relations in timed automata. In In Proc. of LICS'02, pages 177-186, 2002. Google Scholar
  14. Jeanne Ferrante and Charles Rackoff. A decision procedure for the first order theory of real addition with order. SIAM Journal on Computing, 4(1):69-76, 1975. Google Scholar
  15. 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. Google Scholar
  16. Dugald Macpherson. A survey of homogeneous structures. Discrete Mathematics, 311(15):1599–1634, 2011. Google Scholar
  17. Mojżesz Presburger. Über der vollständigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchen die addition als einzige operation hervortritt. Comptes Rendus Premier Congrès des Mathématicienes des Pays Slaves, 395:92-101, 1930. Google Scholar
  18. K. Quaas, M. Shirmohammadi, and J. Worrell. Revisiting reachability in timed automata. In Proc. of LICS'17, pages 1-12, June 2017. URL: http://dx.doi.org/10.1109/LICS.2017.8005098.
  19. Eduardo D. Sontag. Real addition and the polynomial hierarchy. Information Processing Letters, 20(3):115-120, 1985. Google Scholar
  20. Ashutosh Trivedi and Dominik Wojtczak. Recursive timed automata. In Proc. ATVA'10, volume 6252 of LNCS, pages 306-324. Springer, 2010. Google Scholar
  21. Yuya Uezato and Yasuhiko Minamide. Synchronized recursive timed automata. In Proc. of LPAR'15, 2015. Google Scholar
  22. Kumar Neeraj Verma, Helmut Seidl, and Thomas Schwentick. On the complexity of equational Horn clauses. In Proc. CADE-20, 2005, pages 337-352, 2005. URL: http://dx.doi.org/10.1007/11532231_25.
  23. Volker Weispfenning. The complexity of linear problems in fields. Journal of Symbolic Computation, 5(1):3-27, 1988. 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 About DROPS Imprint Privacy Contact