Pushdown timed automata: A binary reachability characterization and safety verification.

DOI10.1016/S0304-3975(02)00743-0zbMath1044.68085OpenAlexW2128090891MaRDI QIDQ1401320

Zhe Dang

Publication date: 17 August 2003

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(02)00743-0

zbMATH Keywords

Real-time systemsTimed automataModel-checkingBinary reachabilityPresburgerPushdown timed automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Related Items (20)

Timed recursive state machines: expressiveness and complexity ⋮ Lossiness of communication channels modeled by transducers1 ⋮ Fast zone-based algorithms for reachability in pushdown timed automata ⋮ Quantifying communication in synchronized languages ⋮ A Logical Characterization of Timed Pushdown Languages ⋮ Quantifying Communication in Synchronized Languages ⋮ Information rate of some classes of non-regular languages: an automata-theoretic approach ⋮ Similarity in languages and programs ⋮ Logics for Weighted Timed Pushdown Automata ⋮ Security of Numerical Sensors in Automata ⋮ A survey of timed automata for the development of real-time systems ⋮ Execution information rate for some classes of automata ⋮ Unnamed Item ⋮ Reachability relations of timed pushdown automata ⋮ Linear reachability problems and minimal solutions to linear Diophantine equation systems ⋮ Reachability results for timed automata with unbounded data structures ⋮ Dense-choice counter machines revisited ⋮ On composition and lookahead delegation of \(e\)-services modeled by automata ⋮ Effective definability of the reachability relation in timed automata ⋮ Sampling automata and programs

Uses Software

• Kronos
• ASTRAL
• HyTech
• Uppaal
• Bebop

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
• Unnamed Item
• ASTRAL
• Model-checking in dense real-time
• Real-time logics: Complexity and expressiveness
• The complexity of decision problems for finite-turn multicounter machines
• A theory of timed automata
• Symbolic model checking for real-time systems
• Uppaal in a nutshell
• From timed automata to logic — and back
• Reversal-Bounded Multicounter Machines and Their Decision Problems
• A really temporal logic
• New Decidability Results Concerning Two-Way Counter Machines
• The benefits of relaxing punctuality
• MULTI-PUSH-DOWN LANGUAGES AND GRAMMARS
• Reachability analysis of pushdown automata: Application to model-checking

This page was built for publication: Pushdown timed automata: A binary reachability characterization and safety verification.