An SMT-based approach to satisfiability checking of MITL
From MaRDI portal
Publication:897649
DOI10.1016/j.ic.2015.06.007zbMath1332.68138OpenAlexW805171677MaRDI QIDQ897649
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
Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)
Related Items (5)
SMT-based satisfiability of first-order LTL with event freezing functions and metric operators ⋮ On the initialization of clocks in timed formalisms ⋮ 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
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Continuous time temporal logic with counting
- Constraint LTL satisfiability checking without automata
- Modeling time in computing.
- An automata-theoretic approach to constraint LTL
- Complexity of metric temporal logics with counting and the Pnueli modalities
- A theory of timed automata
- Timer formulas and decidable metric temporal logic
- On MITL and Alternating Timed Automata
- Completeness of the Bounded Satisfiability Problem for Constraint LTL
- From MITL to Timed Automata
- On the Expressiveness of MTL with Past Operators
- A really temporal logic
- The benefits of relaxing punctuality
- Deciding Continuous-Time Metric Temporal Logic with Counting Modalities
- Expressiveness of Metric modalities for continuous time
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- On MITL and Alternating Timed Automata over Infinite Words
- Lectures on Concurrency and Petri Nets
- FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
This page was built for publication: An SMT-based approach to satisfiability checking of MITL
