Content deleted Content added
Omnipaedista (talk | contribs) No edit summary |
|||
Line 35:
* <math>\gamma,t,\nu\models x\sim c</math> holds if <math>t-\nu(y)\sim c</math>.
== Metric
[[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>.
| |||