Reachability relations of timed pushdown automata
Publication:2221811
DOI10.1016/j.jcss.2020.11.003zbMath1484.68079arXiv2012.15291OpenAlexW3109777388MaRDI QIDQ2221811
Sławomir Lasota, Lorenzo Clemente
Publication date: 2 February 2021
Published in: Journal of Computer and System Sciences (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2012.15291
quantifier eliminationtimed automataPresburger arithmeticrational arithmeticreachability relationclock difference relationstimed pushdown automata
Formal languages and automata (68Q45) Logic in computer science (03B70) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) First-order arithmetic and fragments (03F30)
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Better abstractions for timed automata
- Recursive unsolvability of Post's problem of Tag und other topics in theory of Turing machines
- Real addition and the polynomial hierarchy
- The complexity of linear problems in fields
- Event-clock automata: a determinizable class of timed automata
- A theory of timed automata
- Pushdown timed automata: A binary reachability characterization and safety verification.
- Kronos: A verification tool for real-time systems
- Model checking LTL with regular valuations for pushdown systems
- On timed scope-bounded context-sensitive languages
- Effective definability of the reachability relation in timed automata
- Reachability in two-clock timed automata is PSPACE-complete
- Reachability in pushdown register automata
- Semigroups, Presburger formulas, and languages
- A Logical Characterization for Dense-Time Visibly Pushdown Automata
- Time-Bounded Reachability Problem for Recursive Timed Automata is Undecidable
- A Perfect Class of Context-Sensitive Timed Languages
- Nested Timed Automata
- Dense-Timed Pushdown Automata
- What's decidable about recursive hybrid automata?
- A Machine-Independent Characterization of Timed Languages
- A Logical Characterization of Timed Pushdown Languages
- Verification for Timed Automata extended with Unbounded Discrete Data Structures
- Synchronized Recursive Timed Automata
- Visibly pushdown languages
- Event-Clock Visibly Pushdown Automata
- Alternation
- A Decision Procedure for the First Order Theory of Real Addition with Order
- Timed Pushdown Automata Revisited
- Recursive Timed Automata
- Binary Reachability of Timed-register Pushdown Automata and Branching Vector Addition Systems
- Pushdown Systems with Stack Manipulation
- Well-Structured Pushdown System: Case of Dense Timed Pushdown Automata
- An effective decision procedure for linear arithmetic over the integers and reals
- CONCUR 2004 - Concurrency Theory
- Automated Deduction – CADE-20
- On Context-Free Languages
- Communicating Timed Automata: The More Synchronous, the More Difficult to Verify
- Reachability Analysis of Communicating Pushdown Systems
- FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
- Hybrid Systems: Computation and Control
