Metric temporal reasoning with less than two clocks

We introduce a new way of defining metric temporal logic on a real-numbers flow of time. The idea is based on having semantics which allow us to refer to a single universal clock of arbitrary precision in order to impose metric constraints. This gives us a new metric temporal logic which is very expressive, is natural to use, can be applied in very general situations, affords a wide range of useful abbreviations and operators, has a PSPACE decision procedure, and has the promise of being amenable to standard reasoning techniques. Thus it has many advantages over the existing metric temporal logics. We provide a decision procedure via conversion to a non-metric temporal logic, hence doing metric reasoning with no clocks.

• Publication year

  2010

• Venue

  J. Appl. Non Class. Logics

• Publication date

  2010-01-01

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.3166/jancl.20.437-455
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• A Tableau for Until and Since over Linear Time

  2011cited by this paper
• Dense Time Reasoning via Mosaics

  2009cited by this paper
• 25 Years of Model Checking - History, Achievements, Perspectives

  2008cited by this paper
• Some Recent Results in Metric Temporal Logic

  2008cited by this paper
• MTL with Bounded Variability: Decidability and Complexity

  2008cited by this paper
• Proceedings of the 6th international conference on Formal Modeling and Analysis of Timed Systems

  2008influential reference
• Model checking temporal metric specifications with Trio2Promela

  2007cited by this paper
• On the expressiveness of MTL in the pointwise and continuous semantics

  2007cited by this paper
• On the Expressiveness of MTL Variants over Dense Time

  2007cited by this paper
• Expressiveness of Metric modalities for continuous time

  2006cited by this paper
• Logics for Real Time: Decidability and Complexity

  2004cited by this paper
• Duration Calculus: A Formal Approach to Real-Time Systems

  2004cited by this paper
• Formal Modeling and Analysis of Timed Systems

  2003cited by this paper
• The complexity of the temporal logic with "until" over general linear time

  2003influential reference
• The Mosaic Method for Temporal Logics

  2000cited by this paper
• A Framework for Decidable Metrical Logics

  1999cited by this paper
• The complexity of temporal logic over the reals

  1999cited by this paper
• On the Decidability of Continuous Time Specification Formalisms

  1998cited by this paper
• Duration Calculus, a Logical Approach to Real-Time Systems

  1998cited by this paper
• Compositional Verification of Multi-Agent Systems in Temporal Multi-Epistemic Logic

  1998cited by this paper
• Automated Reasoning with Analytic Tableaux and Related Methods

  1998cited by this paper
• Reasoning about Plans

  1997cited by this paper
• Using interval temporal logic and inference rules for the automatic generation of multimedia presentations

  1996cited by this paper
• Temporal verification of reactive systems - safety

  1995cited by this paper
• Finite Divergence

  1995cited by this paper
• Temporal Verification of Reactive Systems

  1995cited by this paper
• Temporal Logic Mathematical Foundations and Computational Aspects

  1994cited by this paper
• Temporal Veri cation of Simulation andRe nement ?

  1994cited by this paper
• Specifying Timed State Sequences in Powerful Decidable Logics and Timed Automata

  1994cited by this paper
• Temporal Logic: Mathematical Foundations and Computational Aspects Volume 1

  1994cited by this paper
• Temporal Verification of Simulation and Refinement

  1993cited by this paper
• Temporal Databases: Theory, Design, and Implementation

  1993cited by this paper
• An axiomatization for until and since over the reals without the IRR rule

  1992cited by this paper
• Reasoning about plans

  1991cited by this paper
• The Temporal Logic of Reactive and Concurrent Systems

  1991cited by this paper
• Logics and Models of Real Time: A Survey

  1991cited by this paper
• The benefits of relaxing punctuality

  1991influential reference
• An Axiomitization of the Temporal Logic with Until and Since over the Real Numbers

  1990cited by this paper
• Real-time logics: complexity and expressiveness

  1990cited by this paper
• Temporal Logic of Real-time Systems

  1990cited by this paper
• Specifying real-time properties with metric temporal logic

  1990cited by this paper
• A really temporal logic

  1989cited by this paper
• Diodoran Modalities

  1986cited by this paper
• Temporal Databases

  1986cited by this paper
• The decision problem for linear temporal logic

  1985cited by this paper
• The temporal logic of programs

  1977cited by this paper
• Tense logic and the theory of linear order

  1968influential reference
• Journal of Applied Non-Classical Logics

  year unknowncited by this paper

• Metric temporal logic revisited

  2016cites this paper
• A tableau for general linear temporal logic

  2013cites this paper
• Bounded variability of metric temporal logic

  2013cites this paper
• A New Metric Temporal Logic for Hybrid Systems

  2013cites this paper
• A Tableau for Until and Since over Linear Time

  2011cites this paper