Verification in loosely synchronous queue-connected discrete timed automata.

DOI10.1016/S0304-3975(02)00076-2zbMath1044.68096OpenAlexW1981600284MaRDI QIDQ1401187

Oscar H. Ibarra, Pierluigi San Pietro, 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)00076-2

zbMATH Keywords

InvarianceReachabilitySafetyDiscrete timed automataQueue-connected

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Related Items (4)

Eliminating the storage tape in reachability constructions. ⋮ A survey of timed automata for the development of real-time systems ⋮ Context-Bounded Analysis of Concurrent Queue Systems ⋮ Augmenting the discrete timed automaton with other data structures.

Uses Software

• ALGOL 60

Cites Work

• Model-checking in dense real-time
• The complexity of decision problems for finite-turn multicounter machines
• A theory of timed automata
• Analysis of a class of communicating finite state machines
• Symbolic model checking for real-time systems
• A technique for proving decidability of containment and equivalence of linear constraint queries
• Verifying programs with unreliable channels
• On Communicating Finite-State Machines
• Reversal-Bounded Multicounter Machines and Their Decision Problems
• A really temporal logic
• Bounded Algol-Like Languages
• Reachability analysis of pushdown automata: Application to model-checking
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Verification in loosely synchronous queue-connected discrete timed automata.