An SMT-based approach to satisfiability checking of MITL

DOI10.1016/J.IC.2015.06.007MaRDI QIDQ897649zbMATH OpenOpenAlexFDO

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

Publication date 7 December 2015

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ic.2015.06.007

Mathematics Subject Classification ID

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

Recommendations

• Deciding the satisfiability of MITL specifications
• A tool for deciding the satisfiability of continuous-time metric temporal logic
• Revisiting MITL to fix decision procedures
• On MITL and alternating timed automata over infinite words
• Timed-automata-based verification of MITL over signals

Cites work

• scientific article; zbMATH DE number 1424034 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A really temporal logic
• A theory of timed automata
• An automata-theoretic approach to constraint LTL
• Completeness of the bounded satisfiability problem for constraint LTL
• Complexity of metric temporal logics with counting and the Pnueli modalities
• Constraint LTL satisfiability checking without automata
• Continuous time temporal logic with counting
• Deciding continuous-time metric temporal logic with counting modalities
• Deciding the satisfiability of MITL specifications
• Expressiveness of Metric modalities for continuous time
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• From MITL to Timed Automata
• Lectures on Concurrency and Petri Nets
• Modeling time in computing.
• On MITL and alternating timed automata
• On MITL and alternating timed automata over infinite words
• On the Expressiveness of MTL with Past Operators
• The benefits of relaxing punctuality
• Timer formulas and decidable metric temporal logic

Cited in

(10)

• From non-punctuality to non-adjacency: a quest for decidability of timed temporal logics with quantifiers
• On the initialization of clocks in timed formalisms
• Deciding the satisfiability of MITL specifications
• Satisfiability checking for mission-time LTL
• Revisiting MITL to fix decision procedures
• A logical characterization of timed regular languages
• Satisfiability checking for mission-time \textsf{LTL} (MLTL)
• A tool for deciding the satisfiability of continuous-time metric temporal logic
• On MITL and alternating timed automata over infinite words
• SMT-based satisfiability of first-order LTL with event freezing functions and metric operators

Describes a project that uses

Uses Software

• z3
• qtlsolver

This page was built for publication: An SMT-based approach to satisfiability checking of MITL

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