Timed propositional temporal logic

In model checking, a field of computer science, Timed Propositional Temporal Logic (TPTL) is an extension of Linear Temporal Logic (LTL) in which variables are introduced to measure times between two events. For example, while LTL allows to state that each event p is eventually followed by an event q, TPTL furthermore allows to give a time limit for q to occur.

Syntax

The future fragment of TPTL is defined similarly to linear temporal logic, in which furthermore, clock variables can be introduced and compared to constants. Formally, given a set of clocks, MTL is built up from:

  • a finite set of propositional variables AP,
  • the logical operators ¬ and ∨, and
  • the temporal modal operator U,
  • a clock comparison , with , a number and being a comparison operator such as <, , =, or >.
  • a freeze quantification operator , for a TPTL formula with set of clocks .

Furthermore, for an interval, is considered as an abbreviation for ; and similarly for every other kind of intervals.

The logic TPTL+Past[1] is built as the future fragment of TLS and also contains

  • the temporal modal operator S.

Note that the next operator N is not considered to be a part of MTL syntax. It will instead be defined from other operators.

A closed formula is a formula over an empty set of clocks.[2]

Model

Let it intuitively represents a set of time. Let a function which associate to each moment a set of propositions from AP. A model of a TPTL formula is such a function . Usually, is either a timed word or a signal. In those cases, is either a discrete subset or an interval containing 0.

Semantic

Let and as above. Let a set of clocks. Let a clock valuation over .

We are now going to explain what it means that a TPTL formula holds at time for a valuation . This is denoted by . Let and be two formulas over the set of clocks , a formula over the set of clocks , , , a number and being a comparison operator such as <, , =, or >: We first consider formulas whose main operator also belongs to LTL:

  • holds if ,
  • holds if either or
  • holds if either or
  • holds if there exists such that and such that for each , ,
  • holds if there exists such that and such that for each , ,
  • holds if holds,
  • holds if .

Metric temporal logic

Metric temporal logic is another extension of LTL which allow to measure time. Instead of adding variables, it adds an infinity of operators and for an interval of non-negative number. The semantic of the formula at some time is essentially the same than the semantic of the formula , with the constraints that the time at which must hold occurs in the interval .

TPTL is as least as expressive as MTL. Indeed, the MTL formula is equivalent to the TPTL formula where is a new variable.[2]

It follows that any other operator introduced in the page MTL, such as and can also be defined as TPTL formulas.

TPTL is strictly more expressive than MTL[1]:2 both over timed words and over signals. Over timed words, no MTL formula is equivalent to . Over signal, there are no MTL formula equivalent to , which states that the last atomic proposition before time point 1 is an .

Comparison with LTL

A standard (untimed) infinite word is a function from to . We can consider such a word using the set of time , and the function . In this case, for an arbitrary LTL formula, if and only if , where is considered as a TPTL formula with non-strict operator, and is the only function defined on the empty set.

References

  1. Bouyer, Patricia; Chevalier, Fabrice; Markey, Nicolas (2005). "On the Expressiveness of TPTL and MTL". roceedings of the 25th Conference on Foundations of Software Technology and Theoretical Computer Science: 436. doi:10.1007/11590156_3.
  2. Alur, Rajeev; Henzinger, Thomas A. (Jan 1994). "A really temporal logic". Journal of the ACM. 41 (1): 181–203. doi:10.1145/174644.174651.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.