Model checking MITL formulae on timed automata. A logic-based approach

DOI10.1145/3383687MaRDI QIDQ5121277zbMATH OpenOpenAlexWikidataFDO

Authors Claudio Menghi, Marcello M. Bersani, Matteo Rossi, Pierluigi San Pietro

Publication date 11 September 2020

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3383687

zbMATH Keywords

model checkingsignal-based semanticstimed automata

Mathematics Subject Classification ID

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

Recommendations

• Timed-automata-based verification of MITL over signals
• On MITL and alternating timed automata
• \textsc{MightyL}: a compositional translation from MITL to timed automata
• From MITL to Timed Automata
• On MITL and alternating timed automata over infinite words

Cited in

(7)

• \textsc{MightyL}: a compositional translation from MITL to timed automata
• On MITL and alternating timed automata
• On clock-aware LTL properties of timed automata
• Model Checking Metric Temporal Logic over Automata with One Counter
• A translation of the existential model checking problem from MITL to HLTL
• Checking MTL Properties of Discrete Timed Automata via Bounded Model Checking
• Timed-automata-based verification of MITL over signals

This page was built for publication: Model checking MITL formulae on timed automata. A logic-based approach

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