The Library
Binary reachability of timed-register pushdown automata and branching vector addition systems
Tools
Clemente, Lorenzo, Lasota, Sławomir, Lazic, Ranko and Mazowiecki, Filip (2019) Binary reachability of timed-register pushdown automata and branching vector addition systems. ACM Transactions on Computational Logic, 20 (3). pp. 1-31. 14. doi:10.1145/3326161 ISSN 1529-3785.
|
PDF
WRAP-binary-reachability-timed-register-pushdown-automata-vector-Lazic-2019.pdf - Accepted Version - Requires a PDF viewer. Download (1864Kb) | Preview |
Official URL: https://doi.org/10.1145/3326161
Abstract
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.
Item Type: | Journal Article | |||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software T Technology > TJ Mechanical engineering and machinery |
|||||||||||||||||||||
Divisions: | Faculty of Science, Engineering and Medicine > Science > Computer Science | |||||||||||||||||||||
SWORD Depositor: | Library Publications Router | |||||||||||||||||||||
Library of Congress Subject Headings (LCSH): | Machine theory, Real-time control, Automatic control, Real-time data processing | |||||||||||||||||||||
Journal or Publication Title: | ACM Transactions on Computational Logic | |||||||||||||||||||||
Publisher: | Association for Computing Machinery (ACM) | |||||||||||||||||||||
ISSN: | 1529-3785 | |||||||||||||||||||||
Official Date: | June 2019 | |||||||||||||||||||||
Dates: |
|
|||||||||||||||||||||
Volume: | 20 | |||||||||||||||||||||
Number: | 3 | |||||||||||||||||||||
Page Range: | pp. 1-31 | |||||||||||||||||||||
Article Number: | 14 | |||||||||||||||||||||
DOI: | 10.1145/3326161 | |||||||||||||||||||||
Status: | Peer Reviewed | |||||||||||||||||||||
Publication Status: | Published | |||||||||||||||||||||
Reuse Statement (publisher, data, author rights): | © Owner/Author | ACM 2019. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in ACM Transactions on Computational Logic, http://dx.doi.org/10.1145/10.1145/3326161 | |||||||||||||||||||||
Access rights to Published version: | Restricted or Subscription Access | |||||||||||||||||||||
Date of first compliant deposit: | 1 July 2019 | |||||||||||||||||||||
Date of first compliant Open Access: | 2 July 2019 | |||||||||||||||||||||
RIOXX Funder/Project Grant: |
|
|||||||||||||||||||||
Related URLs: |
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |
Downloads
Downloads per month over past year