Content deleted Content added
Correction of a wrong negation |
m Typo fixing, typo(s) fixed: Indeed → Indeed, |
||
Line 16:
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.<ref name="Really">{{cite journal |last1=Alur |first1=Rajeev |last2=Henzinger |first2=Thomas A. |title=A really temporal logic|journal=Journal of the ACM (JACM|date=Jan 1994 |volume=41 |issue =1|
== Model ==
Line 38:
[[Metric temporal logic]] is another extension of LTL which allow to measure time. Instead of adding variables, it adds an infinity of operators <math>\mathcal U_I</math> and <math>\mathcal S_I</math> for <math>I</math> an interval of non-negative number. The semantic of the formula <math>\phi\mathcal U_I\psi</math> at some time <math>t</math> is essentially the same than the semantic of the formula <math>\phi\mathcal U\psi</math>, with the constraints that the time <math>t''</math> at which <math>\psi</math> must hold occurs in the interval <math>t+I</math>.
TPTL is as least as expressive as MTL. Indeed, the MTL formula <math>\phi\mathcal U_I\psi</math> is equivalent to the TPTL formula <math>x.\phi\mathcal(x\in I\land\psi)</math> where <math>x</math> is a new variable.<ref name="Really"/>
It follows that any other operator introduced in the page [[metric temporal logic#Operators defined from MTL operator|MTL]], such as <math>\Box</math> and <math>\Diamond</math> can also be defined as TPTL formulas.
| |||