From real-time logic to timed automata

DOI10.1145/3286976MaRDI QIDQ5215449zbMATH OpenOpenAlexWikidataFDO

Authors Thomas Ferrère, Oded Maler, Dejan Ničković, Amir Pnueli

Publication date 11 February 2020

Published in Journal of the ACM (Search for Journal in Brave)

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

zbMATH Keywords

formal verificationmodel checkingreal-timetemporal logictimed automata

Mathematics Subject Classification ID

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

Recommendations

• From MITL to Timed Automata
• \textsc{MightyL}: a compositional translation from MITL to timed automata
• Timed-automata-based verification of MITL over signals
• Translating a continuous-time temporal logic into timed automata.
• From \textsc{mtl} to deterministic timed automata

Cited in

(14)

• Algebraic quantitative semantics for efficient online temporal monitoring
• \textsc{MightyL}: a compositional translation from MITL to timed automata
• Automata and temporal logic over arbitrary linear time
• On construction of safety signal automata for \(\mathrm{MITL}[\mathcal{U},\mathcal{S}]\) using temporal projections
• Decidability and Expressive Power of Real Time Logics
• From MITL to Timed Automata
• From \textsc{mtl} to deterministic timed automata
• scientific article; zbMATH DE number 2112984 (Why is no real title available?)
• Translating a continuous-time temporal logic into timed automata.
• Decidability of the initial-state opacity of real-time automata
• Timed-automata-based verification of MITL over signals
• Online monitoring of metric temporal logic using sequential networks
• MITL model checking via generalized timed automata and a new liveness algorithm
• Runtime enforcement of CPS against signal temporal logic

This page was built for publication: From real-time logic to timed automata

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