Generalized discrete timed automata: Decidable approximations for safety verification.

DOI10.1016/S0304-3975(02)00432-2zbMath1044.68086OpenAlexW1964178654MaRDI QIDQ1401259

Oscar H. Ibarra, Richard A. Kemmerer, 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)00432-2

zbMATH Keywords

\(\langle B,r\rangle\)-crossing-bounded approximation\(B\)-bounded approximation\(r\)-reset-bounded approximation

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Related Items (2)

Modeling and verification of hybrid dynamic systems using multisingular hybrid Petri nets ⋮ On composition and lookahead delegation of \(e\)-services modeled by automata

Uses Software

• Kronos
• ASTRAL
• Uppaal

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• ASTRAL
• Model-checking in dense real-time
• A theory of timed automata
• Symbolic model checking for real-time systems
• Kronos: A verification tool 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
• Parametric real-time reasoning

This page was built for publication: Generalized discrete timed automata: Decidable approximations for safety verification.