A tool for deciding the satisfiability of continuous-time metric temporal logic
From MaRDI portal
Publication:262137
DOI10.1007/S00236-015-0229-YzbMATH Open1336.68230OpenAlexW2086023301MaRDI QIDQ262137FDOQ262137
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
Recommendations
Cites Work
- A theory of timed automata
- Complexity, convexity and combinations of theories
- 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
- Title not available (Why is that?)
- Constraint LTL satisfiability checking without automata
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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
- Title not available (Why is that?)
- Verification, Model Checking, and Abstract Interpretation
- Axioms for real-time logics
- 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
Cited In (9)
- On the initialization of clocks in timed formalisms
- PuRSUE -- from specification of robotic environments to synthesis of controllers
- The compound interest in relaxing punctuality
- A logical characterization of timed regular languages
- Integrating Discrete- and Continuous-Time Metric Temporal Logics Through Sampling
- Theorem proving for pointwise metric temporal logic over the naturals via translations
- qtlsolver
- Using formal verification to evaluate the execution time of Spark applications
- A Tool That Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic
Uses Software
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)
