From MITL to Timed Automata

DOI10.1007/11867340_20MaRDI QIDQ3511242zbMATH OpenOpenAlexFDO

Authors Oded Maler, Dejan Ničković, Amir Pnueli

Publication date 8 July 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11867340_20

Mathematics Subject Classification ID

Temporal logic (03B44) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• From real-time logic to timed automata
• \textsc{MightyL}: a compositional translation from MITL to timed automata
• Timed-automata-based verification of MITL over signals
• On MITL and alternating timed automata
• From \textsc{mtl} to deterministic timed automata

Cited in

(36)

• On the timed temporal logic planning of coupled multi-agent systems
• Robust control for signal temporal logic specifications using discrete average space robustness
• The compound interest in relaxing punctuality
• Iterative bounded synthesis for efficient cycle detection in parametric timed automata
• Algebraic quantitative semantics for efficient online temporal monitoring
• \textsc{MightyL}: a compositional translation from MITL to timed automata
• A brief account of runtime verification
• Bounded variability of metric temporal logic
• A tool for deciding the satisfiability of continuous-time metric temporal logic
• Metric temporal logic revisited
• On MITL and alternating timed automata
• On construction of safety signal automata for \(\mathrm{MITL}[\mathcal{U},\mathcal{S}]\) using temporal projections
• MTL with Bounded Variability: Decidability and Complexity
• From \textsc{mtl} to deterministic timed automata
• Checking timed Büchi automata emptiness using LU-abstractions
• MR4UM: a framework for adding fault tolerance to UML state diagrams
• scientific article; zbMATH DE number 139828 (Why is no real title available?)
• Runtime enforcement of timed properties revisited
• Model checking MITL formulae on timed automata. A logic-based approach
• From real-time logic to timed automata
• scientific article; zbMATH DE number 7056237 (Why is no real title available?)
• Checking Temporal Properties of Discrete, Timed and Continuous Behaviors
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• On MITL and alternating timed automata over infinite words
• scientific article; zbMATH DE number 5499354 (Why is no real title available?)
• Real-time policy enforcement with metric first-order temporal logic
• Pattern Matching and Parameter Identification for Parametric Timed Regular Expressions
• Timed-automata-based verification of MITL over signals
• Robust satisfaction of metric interval temporal logic objectives in adversarial environments
• Online monitoring of metric temporal logic using sequential networks
• MITL model checking via generalized timed automata and a new liveness algorithm
• BT2automata: expressing behavior trees as automata for formal control synthesis
• Monitoring spatially distributed cyber-physical systems with alternating finite automata
• Counterfactual explanations for MITL violations
• Enforcing spatio-temporal collaborations in distributed predictive control under temporally relaxed STL specifications
• An SMT-based approach to satisfiability checking of MITL

This page was built for publication: From MITL to Timed Automata

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