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

DOI10.1016/S0304-3975(02)00743-0zbMATH Open1044.68085OpenAlexW2128090891MaRDI QIDQ1401320FDOQ1401320

Authors: 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

Recommendations

• scientific article; zbMATH DE number 1796157
• scientific article; zbMATH DE number 1670769
• Past pushdown timed automata and safety verification.
• Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms
• Reachability relations of timed pushdown automata

zbMATH Keywords

Real-time systemsTimed automataModel-checkingBinary reachabilityPresburgerPushdown timed automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Cites Work

• ASTRAL
• Uppaal in a nutshell
• A theory of timed automata
• Title not available (Why is that?)
• Reversal-Bounded Multicounter Machines and Their Decision Problems
• A really temporal logic
• The benefits of relaxing punctuality
• Title not available (Why is that?)
• Model-checking in dense real-time
• Real-time logics: Complexity and expressiveness
• Symbolic model checking for real-time systems
• From timed automata to logic -- and back
• Title not available (Why is that?)
• The complexity of decision problems for finite-turn multicounter machines
• Title not available (Why is that?)
• MULTI-PUSH-DOWN LANGUAGES AND GRAMMARS
• Reachability analysis of pushdown automata: Application to model-checking
• Title not available (Why is that?)
• Title not available (Why is that?)
• New Decidability Results Concerning Two-Way Counter Machines
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (26)

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

Uses Software

• Kronos
• ASTRAL
• HyTech
• Uppaal
• Bebop

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

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