{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:28:41Z","timestamp":1750220921691,"version":"3.41.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T00:00:00Z","timestamp":1559260800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100008952","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-10-IDEX-03-02"],"award-info":[{"award-number":["ANR-10-IDEX-03-02"]}],"id":[{"id":"10.13039\/501100008952","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/M011801\/1"],"award-info":[{"award-number":["EP\/M011801\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004281","name":"Narodowe Centrum Nauki","doi-asserted-by":"publisher","award":["2016\/21\/B\/ST6\/01505, 2017\/26\/D\/ST6\/00201"],"award-info":[{"award-number":["2016\/21\/B\/ST6\/01505, 2017\/26\/D\/ST6\/00201"]}],"id":[{"id":"10.13039\/501100004281","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100011199","name":"European Research Council","doi-asserted-by":"publisher","award":["683080"],"award-info":[{"award-number":["683080"]}],"id":[{"id":"10.13039\/100011199","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000275","name":"Leverhulme Trust","doi-asserted-by":"publisher","award":["RF-2017-579"],"award-info":[{"award-number":["RF-2017-579"]}],"id":[{"id":"10.13039\/501100000275","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2019,7,31]]},"abstract":"<jats:p>Timed-register pushdown automata constitute a very expressive class of automata, whose transitions may involve state, input, and top-of-stack timed registers with unbounded differences. They strictly subsume pushdown timed automata of Bouajjani et al., dense-timed pushdown automata of Abdulla et al., and orbit-finite timed-register pushdown automata of Clemente and Lasota. We give an effective logical characterisation of the reachability relation of timed-register pushdown automata. As a corollary, we obtain a doubly exponential time procedure for the non-emptiness problem. We show that the complexity reduces to singly exponential under the assumption of monotonic time. The proofs involve a novel model of one-dimensional integer branching vector addition systems with states. As a result interesting on its own, we show that reachability sets of the latter model are semilinear and computable in exponential time.<\/jats:p>","DOI":"10.1145\/3326161","type":"journal-article","created":{"date-parts":[[2019,6,3]],"date-time":"2019-06-03T12:23:16Z","timestamp":1559564596000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Binary Reachability of Timed-register Pushdown Automata and Branching Vector Addition Systems"],"prefix":"10.1145","volume":"20","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0578-9103","authenticated-orcid":false,"given":"Lorenzo","family":"Clemente","sequence":"first","affiliation":[{"name":"Wydzia\u0142 Matematyki, Informatyki i Mechaniki, University of Warsaw, Banacha, Warsaw, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S\u0142awomir","family":"Lasota","sequence":"additional","affiliation":[{"name":"Wydzia\u0142 Matematyki, Informatyki i Mechaniki, University of Warsaw, Banacha, Warsaw, Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ranko","family":"Lazi\u0107","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Warwick, Coventry, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Filip","family":"Mazowiecki","sequence":"additional","affiliation":[{"name":"LABRI, Universit\u00e9 de Bordeaux, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,5,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.15"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the CONCUR\u201916","author":"Akshay S.","year":"2016","unstructured":"S. Akshay , Paul Gastin , and Shankara Narayanan Krishna . 2016 . Analyzing timed systems using tree automata . In Proceedings of the CONCUR\u201916 . 27:1--27:14. S. Akshay, Paul Gastin, and Shankara Narayanan Krishna. 2016. Analyzing timed systems using tree automata. In Proceedings of the CONCUR\u201916. 27:1--27:14."},{"volume-title":"The Diophantine Frobenius Problem","author":"Ram\u00edrez Alfons\u00edn J. L.","key":"e_1_2_1_3_1","unstructured":"J. L. Ram\u00edrez Alfons\u00edn . 2005. The Diophantine Frobenius Problem . Oxford University Press . J. L. Ram\u00edrez Alfons\u00edn. 2005. The Diophantine Frobenius Problem. Oxford University Press."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2010.10"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.02.021"},{"key":"e_1_2_1_7_1","unstructured":"Miko\u0142aj Boja\u0144czyk. 2017. Slightly Infinite Sets. Retrieved from https:\/\/www.mimuw.edu.pl\/ bojan\/paper\/atom-book.  Miko\u0142aj Boja\u0144czyk. 2017. Slightly Infinite Sets. Retrieved from https:\/\/www.mimuw.edu.pl\/ bojan\/paper\/atom-book."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(3:4)2014"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31585-5_12"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/647763.735668"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/646875.710005"},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the CSL\u201915 (LIPIcs)","volume":"41","author":"Clemente Lorenzo","year":"2015","unstructured":"Lorenzo Clemente and Slawomir Lasota . 2015 . Reachability analysis of first-order definable pushdown systems . In Proceedings of the CSL\u201915 (LIPIcs) , Vol. 41 . Dagstuhl, 244--259. Lorenzo Clemente and Slawomir Lasota. 2015. Reachability analysis of first-order definable pushdown systems. In Proceedings of the CSL\u201915 (LIPIcs), Vol. 41. Dagstuhl, 244--259."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.73"},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the ICALP\u201918","author":"Clemente Lorenzo","year":"2018","unstructured":"Lorenzo Clemente and Slawomir Lasota . 2018 . Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms . In Proceedings of the ICALP\u201918 . Lorenzo Clemente and Slawomir Lasota. 2018. Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms. In Proceedings of the ICALP\u201918."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/3329995.3330018"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.12.004"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the ICALP\u201917","author":"Figueira Diego","year":"2017","unstructured":"Diego Figueira , Ranko Lazic , Jerome Leroux , Filip Mazowiecki , and Gr\u00e9goire Sutre . 2017 . Polynomial-space completeness of reachability for succinct branching VASS in dimension one . In Proceedings of the ICALP\u201917 . Diego Figueira, Ranko Lazic, Jerome Leroux, Filip Mazowiecki, and Gr\u00e9goire Sutre. 2017. Polynomial-space completeness of reachability for succinct branching VASS in dimension one. In Proceedings of the ICALP\u201917."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1966.16.285"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the ICALP\u201916 (LIPIcs)","volume":"55","author":"G\u00f6ller Stefan","year":"2016","unstructured":"Stefan G\u00f6ller , Christoph Haase , Ranko Lazi\u0107 , and Patrick Totzke . 2016 . A polynomial-time algorithm for reachability in branching VASS in dimension one . In Proceedings of the ICALP\u201916 (LIPIcs) , Vol. 55 . Dagstuhl. Stefan G\u00f6ller, Christoph Haase, Ranko Lazi\u0107, and Patrick Totzke. 2016. A polynomial-time algorithm for reachability in branching VASS in dimension one. In Proceedings of the ICALP\u201916 (LIPIcs), Vol. 55. Dagstuhl."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-008-9139-5"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2010.06.008"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603129"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.disc.2011.01.024"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90044-2"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/321356.321364"},{"key":"e_1_2_1_26_1","unstructured":"Moj\u017cesz Presburger. 1930. \u00dcber der Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen in welchen die Addition als einzige Operation hervortritt. Comptes Rendus Premier Congr\u00e8s des Math\u00e9maticienes des Pays Slaves 395 (1930) 92--101.  Moj\u017cesz Presburger. 1930. \u00dcber der Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen in welchen die Addition als einzige Operation hervortritt. Comptes Rendus Premier Congr\u00e8s des Math\u00e9maticienes des Pays Slaves 395 (1930) 92--101."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/1927331.1927356"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.46298\/dmtcs.350"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_25"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3326161","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3326161","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:08Z","timestamp":1750204388000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3326161"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,5,31]]},"references-count":29,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,7,31]]}},"alternative-id":["10.1145\/3326161"],"URL":"https:\/\/doi.org\/10.1145\/3326161","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2019,5,31]]},"assertion":[{"value":"2018-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-05-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}