Timed Pushdown Automata Revisited

DOI10.1109/LICS.2015.73MaRDI QIDQ4635851zbMATH OpenOpenAlexWikidataFDO

Authors Lorenzo Clemente, Sławomir Lasota

Publication date 23 April 2018

Published in 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1503.02422

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Formal languages and automata (68Q45)

Abstract: This paper contains two results on timed extensions of pushdown automata (PDA). As our first result we prove that the model of dense-timed PDA of Abdulla et al. collapses: it is expressively equivalent to dense-timed PDA with timeless stack. Motivated by this result, we advocate the framework of first-order definable PDA, a specialization of PDA in sets with atoms, as the right setting to define and investigate timed extensions of PDA. The general model obtained in this way is Turing complete. As our second result we prove NEXPTIME upper complexity bound for the non-emptiness problem for an expressive subclass. As a byproduct, we obtain a tight EXPTIME complexity bound for a more restrictive subclass of PDA with timeless stack, thus subsuming the complexity bound known for dense-timed PDA.

Recommendations

• Decomposing timed push down automata
• scientific article; zbMATH DE number 1949647
• Timed P Automata
• Timed P automata
• Timed P Automata
• Dense-timed pushdown automata
• Reachability relations of timed pushdown automata
• Time varying pushdown automata
• scientific article; zbMATH DE number 1189294
• scientific article; zbMATH DE number 7297846

Cited in

(26)

• Adding dense-timed stack to integer reset timed automata
• Dynamic data structures for timed automata acceptance
• On the determinization of event-clock input-driven pushdown automata
• Context-free timed formalisms: robust automata and linear temporal logics
• Reachability relations of timed pushdown automata
• Reachability in two-clock timed automata is PSPACE-complete
• Timed recursive state machines: expressiveness and complexity
• Decomposing timed push down automata
• Tinput-Driven Pushdown Automata
• Dense-timed pushdown automata
• A logical characterization of timed pushdown languages
• Timed context-free temporal logics
• Event-Clock Visibly Pushdown Automata
• scientific article; zbMATH DE number 1189294 (Why is no real title available?)
• scientific article; zbMATH DE number 1973972 (Why is no real title available?)
• Analyzing timed systems using tree automata
• Zenoness for timed pushdown automata
• Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms
• Verifying quantitative temporal properties of procedural programs
• Towards an Efficient Tree Automata based technique for Timed Systems
• Timed pushdown automata and branching vector addition systems
• Well-structured pushdown system: case of dense timed pushdown automata
• Timed P Automata
• scientific article; zbMATH DE number 7156375 (Why is no real title available?)
• scientific article; zbMATH DE number 5201490 (Why is no real title available?)
• Fast zone-based algorithms for reachability in pushdown timed automata

This page was built for publication: Timed Pushdown Automata Revisited

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4635851)