English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Open

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.

Binary Reachability of Timed-register Pushdown Automata and Branching Vector Addition Systems