MITL model checking via generalized timed automata and a new liveness algorithm

DOI10.4230/LIPICS.CONCUR.2024.5MaRDI QIDQ6859954zbMATH OpenFDO

Authors S. Akshay, Paul Gastin, Rahul Govind, B. Srivathsan

Publication date 10 February 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.4230/LIPICS.CONCUR.2024.5

zbMATH Keywords

livenessMITL model checkingtimed automatazones

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites work

• \textsc{MightyL}: a compositional translation from MITL to timed automata
• A theory of timed automata
• A unified model for real-time systems: symbolic techniques and implementation
• An automata-theoretic approach to linear temporal logic
• Better abstractions for timed automata
• Checking timed Büchi automata emptiness efficiently
• Checking timed Büchi automata emptiness using LU-abstractions
• Complexity issues for timeline-based planning over dense time under future and minimal semantics
• Efficient emptiness check for timed Büchi automata
• Event-clock automata: a determinizable class of timed automata
• Fast algorithms for handling diagonal constraints in timed automata
• Foundations of Software Science and Computation Structures
• From MITL to Timed Automata
• From real-time logic to timed automata
• scientific article; zbMATH DE number 3982506 (Why is no real title available?)
• scientific article; zbMATH DE number 4128370 (Why is no real title available?)
• scientific article; zbMATH DE number 1069484 (Why is no real title available?)
• scientific article; zbMATH DE number 1796123 (Why is no real title available?)
• scientific article; zbMATH DE number 2102731 (Why is no real title available?)
• MITL model checking via generalized timed automata and a new liveness algorithm
• On MITL and alternating timed automata
• On MITL and alternating timed automata over infinite words
• On regions and zones for event-clock automata
• Reachability in timed automata with diagonal constraints
• The benefits of relaxing punctuality
• Why liveness for timed automata is hard, and what we can do about it

Cited in

(3)

• MITL model checking via generalized timed automata and a new liveness algorithm
• Model-checking real-time systems: revisiting the alternating automaton route
• BT2automata: expressing behavior trees as automata for formal control synthesis

This page was built for publication: MITL model checking via generalized timed automata and a new liveness algorithm

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