2026-08-16T20:06:20Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9122 2024-03-06T10:43:25Z ddc:004 open_access

Binary Reachability of Timed Pushdown Automata via Quantifier Elimination and Cyclic Order Atoms Clemente, Lorenzo Lasota, Slawomir timed automata reachability relation timed pushdown automata linear arithmetic 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Lorenzo Clemente and Slawomir Lasota 2018 Is Part Of LIPIcs, Volume 107, 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ICALP.2018.118 urn:nbn:de:0030-drops-91228 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.118 eng https://creativecommons.org/licenses/by/3.0/legalcode