A tool for deciding the satisfiability of continuous-time metric temporal logic

DOI10.1007/S00236-015-0229-YMaRDI QIDQ262137zbMATH OpenOpenAlexFDO

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

Publication date 29 March 2016

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/11311/964235

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Temporal logic (03B44)

Recommendations

• Deciding the satisfiability of MITL specifications
• An SMT-based approach to satisfiability checking of MITL
• Deciding continuous-time metric temporal logic with counting modalities
• A logical characterization of timed regular languages
• Constraint LTL satisfiability checking without automata

Cites work

• scientific article; zbMATH DE number 1973987 (Why is no real title available?)
• scientific article; zbMATH DE number 2112984 (Why is no real title available?)
• scientific article; zbMATH DE number 3068536 (Why is no real title available?)
• A Decision Procedure for the First Order Theory of Real Addition with Order
• A logical characterization of timed (non-)regular languages
• A theory of timed automata
• An SMT-based approach to satisfiability checking of MITL
• An automata-theoretic approach to constraint LTL
• Axioms for real-time logics
• Completeness of the bounded satisfiability problem for constraint LTL
• Complexity of metric temporal logics with counting and the Pnueli modalities
• Complexity, convexity and combinations of theories
• Constraint LTL satisfiability checking without automata
• Deciding continuous-time metric temporal logic with counting modalities
• Deciding the satisfiability of MITL specifications
• Exact Incremental Analysis of Timed Automata with an SMT-Solver
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• From MITL to Timed Automata
• Lectures on Concurrency and Petri Nets
• Linear Encodings of Bounded LTL Model Checking
• On the expressiveness of TPTL and MTL
• Polynomial algorithms in linear programming
• Simplification by Cooperating Decision Procedures
• The benefits of relaxing punctuality
• Timer formulas and decidable metric temporal logic
• Verification of timed automata via satisfiability checking
• Verification, Model Checking, and Abstract Interpretation

Cited in

(14)

• Theorem proving for pointwise metric temporal logic over the naturals via translations
• On the initialization of clocks in timed formalisms
• The compound interest in relaxing punctuality
• Deciding the satisfiability of MITL specifications
• Using formal verification to evaluate the execution time of Spark applications
• A logical characterization of timed (non-)regular languages
• Deciding continuous-time metric temporal logic with counting modalities
• An SMT-based approach to satisfiability checking of MITL
• qtlsolver
• A logical characterization of timed regular languages
• Integrating Discrete- and Continuous-Time Metric Temporal Logics Through Sampling
• Satisfiability checking for mission-time \textsf{LTL} (MLTL)
• PuRSUE -- from specification of robotic environments to synthesis of controllers
• A Tool That Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic

Describes a project that uses

Uses Software

• z3
• zot

This page was built for publication: A tool for deciding the satisfiability of continuous-time metric temporal logic

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