Presburger liveness verification of discrete timed automata.

DOI10.1016/S0304-3975(02)00485-1zbMath1040.68050MaRDI QIDQ1874402

Zhe Dang, Richard A. Kemmerer, Pierluigi San Pietro

Publication date: 25 May 2003

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

zbMATH Keywords

Temporal logicTimed automataLivenessModel-checking

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Related Items (7)

Model-checking CTL* over flat Presburger counter systems ⋮ An automata-theoretic approach to constraint LTL ⋮ Verification of qualitative \(\mathbb Z\) constraints ⋮ Linear reachability problems and minimal solutions to linear Diophantine equation systems ⋮ LTL over integer periodicity constraints ⋮ Linear-time temporal logics with Presburger constraints: an overview ★ ⋮ On composition and lookahead delegation of \(e\)-services modeled by automata

Uses Software

• Kronos
• ASTRAL
• HyTech
• Uppaal

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model-checking in dense real-time
• Real-time logics: Complexity and expressiveness
• The complexity of almost linear diophantine problems
• 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
• The benefits of relaxing punctuality
• What good are digital clocks?

This page was built for publication: Presburger liveness verification of discrete timed automata.