Reachability relations of timed pushdown automata
DOI10.1016/j.jcss.2020.11.003zbMath1484.68079arXiv2012.15291MaRDI 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 elimination; timed automata; Presburger arithmetic; rational arithmetic; reachability relation; clock difference relations; timed pushdown automata
68Q45: Formal languages and automata
03B70: Logic in computer science
03D05: Automata and formal grammars in connection with logical questions
68Q60: Specification and verification (program logics, model checking, etc.)
03F30: First-order arithmetic and fragments
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
