Timed propositional temporal logic: Difference between revisions

Revision as of 08:15, 22 March 2019

Revision as of 13:30, 28 March 2019

Line 35:

* <math>\gamma,t,\nu\models x\sim c</math> holds if <math>t-\nu(y)\sim c</math>.

== From Metric Temporal Logic to TPTL ==

[[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>.

TheTPTL 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.

It is believed that TPTL is strictly more expressive than MTL{{r|ExpressivenesOfTPTLAndMtl|p=2}}. No MTL formula equivalent to <math>\Box(p\implies x.\Diamond(q\land\Diamond(r\land x\le 5)))</math> is known. However, it has not been proven either that no such formula exists.

== Comparison with LTL ==