Timed propositional temporal logic: Difference between revisions

Revision as of 19:26, 6 February 2025

Revision as of 19:27, 6 February 2025

Line 36:

== Metric temporal logic ==

[[Metric temporal logic]] is another extension of LTL that allows measurement of 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 numbernumbers. The semantics of the formula <math>\phi \mathbin\mathcal {U_I}\psi</math> at some time <math>t</math> is essentially the same than the semantics of the formula <math>\phi \mathbin\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\mathbin\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"/>