An SMT-based approach to satisfiability checking of MITL

DOI10.1016/J.IC.2015.06.007zbMATH Open1332.68138OpenAlexW805171677MaRDI QIDQ897649FDOQ897649

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

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

Mathematics Subject Classification ID

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

Cites Work

• A theory of timed automata
• Timer formulas and decidable metric temporal logic
• Completeness of the bounded satisfiability problem for constraint LTL
• From MITL to Timed Automata
• A really temporal logic
• The benefits of relaxing punctuality
• Constraint LTL satisfiability checking without automata
• Title not available (Why is that?)
• Deciding Continuous-Time Metric Temporal Logic with Counting Modalities
• Expressiveness of Metric modalities for continuous time
• Title not available (Why is that?)
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Lectures on Concurrency and Petri Nets
• FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
• An automata-theoretic approach to constraint LTL
• Complexity of metric temporal logics with counting and the Pnueli modalities
• Continuous time temporal logic with counting
• Title not available (Why is that?)
• Modeling time in computing.
• On MITL and Alternating Timed Automata over Infinite Words
• On MITL and alternating timed automata
• On the Expressiveness of MTL with Past Operators

Cited In (6)

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

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)