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

DOI10.1142/S0129054102001539zbMATH Open1067.68090OpenAlexW1546494787MaRDI QIDQ3021995FDOQ3021995

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

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

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)

Cites Work

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

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)