THE EXISTENCE OF ω-CHAINS FOR TRANSITIVE MIXED LINEAR RELATIONS AND ITS APPLICATIONS

DOI10.1142/S0129054102001539MaRDI QIDQ3021995zbMATHOpenAlexFDO

Authors Zhe Dang, Oscar H. Ibarra

Publication date 22 June 2005

Published in International Journal of Foundations of Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1142/s0129054102001539

zbMATH Keywords

timed automatasafetyliveness\(\omega\)-chainsmixed linear relations

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Presburger liveness verification of discrete timed automata.
• scientific article; zbMATH DE number 1689043
• Why liveness for timed automata is hard, and what we can do about it
• Why liveness for timed automata is hard, and what we can do about it
• Finite automata on timed \(\omega\)-trees

Cites work

• A really temporal logic
• A theory of timed automata
• Model-checking in dense real-time
• Reversal-Bounded Multicounter Machines and Their Decision Problems
• Symbolic model checking for real-time systems
• The complexity of decision problems for finite-turn multicounter machines
• Uppaal in a nutshell

Cited in

(1)

• Verification of qualitative \(\mathbb Z\) constraints

This page was built for publication: THE EXISTENCE OF ω-CHAINS FOR TRANSITIVE MIXED LINEAR RELATIONS AND ITS APPLICATIONS

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