On the expressiveness of TPTL and MTL

DOI10.1016/j.ic.2009.10.004zbMath1209.03010OpenAlexW2047923159MaRDI QIDQ2266987

Fabrice Chevalier, Nicolas Markey, Patricia Bouyer

Publication date: 26 February 2010

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2009.10.004

zbMATH Keywords

expressivenesslinear-time temporal logicinterval-based semanticsmetric temporal logic MTLpointwise semanticstimed propositional temporal logic TPTL

Mathematics Subject Classification ID

Temporal logic (03B44)

Related Items (10)

Time-Bounded Verification of CTMCs against Real-Time Specifications ⋮ Model Checking Real-Time Systems ⋮ SMT-based satisfiability of first-order LTL with event freezing functions and metric operators ⋮ Linear Time Monitoring for One Variable TPTL ⋮ Unnamed Item ⋮ Almost event-rate independent monitoring ⋮ Timed modal logics for real-time systems. Specification, verification and control ⋮ Model checking restricted sets of timed paths ⋮ From Nondeterministic to Multi-Head Deterministic Finite-State Transducers ⋮ A tool for deciding the satisfiability of continuous-time metric temporal logic

Cites Work

• About the expressive power of CTL combinators
• Model-checking in dense real-time
• Real-time logics: Complexity and expressiveness
• A theory of timed automata
• Symbolic model checking for real-time systems
• The complexity of the temporal logic with ``until over general linear time
• Model checking restricted sets of timed paths
• On the Expressiveness of MTL Variants over Dense Time
• On the Expressiveness of MTL with Past Operators
• “Sometimes” and “not never” revisited
• The complexity of propositional linear temporal logics
• A really temporal logic
• The benefits of relaxing punctuality
• Expressiveness of Metric modalities for continuous time
• An Expressive Temporal Logic for Real Time
• CONCUR 2005 – Concurrency Theory
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On the expressiveness of TPTL and MTL