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

DOI10.1007/s00236-015-0229-yzbMath1336.68230OpenAlexW2086023301MaRDI QIDQ262137

Matteo Rossi, Marcello M. Bersani, 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)

Related Items

PuRSUE -- from specification of robotic environments to synthesis of controllers ⋮ 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 ⋮ A logical characterization of timed regular languages ⋮ qtlsolver ⋮ Using formal verification to evaluate the execution time of Spark applications

Uses Software

• z3
• zot

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Constraint LTL satisfiability checking without automata
• An automata-theoretic approach to constraint LTL
• An SMT-based approach to satisfiability checking of MITL
• Complexity of metric temporal logics with counting and the Pnueli modalities
• Complexity, convexity and combinations of theories
• A theory of timed automata
• Timer formulas and decidable metric temporal logic
• On the expressiveness of TPTL and MTL
• A Logical Characterization of Timed (non-)Regular Languages
• Exact Incremental Analysis of Timed Automata with an SMT-Solver
• Completeness of the Bounded Satisfiability Problem for Constraint LTL
• From MITL to Timed Automata
• Simplification by Cooperating Decision Procedures
• Polynomial algorithms in linear programming
• A Decision Procedure for the First Order Theory of Real Addition with Order
• The benefits of relaxing punctuality
• Deciding Continuous-Time Metric Temporal Logic with Counting Modalities
• Linear Encodings of Bounded LTL Model Checking
• Verification of Timed Automata via Satisfiability Checking
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Lectures on Concurrency and Petri Nets
• Verification, Model Checking, and Abstract Interpretation
• Axioms for real-time logics