Timed propositional temporal logic: Difference between revisions

Revision as of 13:42, 13 June 2023

Revision as of 18:24, 13 June 2023

Line 6:

* the [[logical connective|logical operators]] ¬ and ∨, and

* the [[Temporal logic|temporal]] [[modal operator]] '''U''',

* a clock comparison <math>x\sim c</math>, with <math>x\in X</math>, <math>c</math> a number and <math>\sim</math> being a comparison operator such as &lt;, &le;, =, &ge; or &gt;.

* a freeze quantification operator <math>x.\phi</math>, for <math>\phi</math> a TPTL formula with set of clocks <math>X\cup\{x\}</math>.

Line 18:

A '''closed formula''' is a formula over an empty set of clocks.<ref name="Really">{{cite journal |last1=Alur |first1=Rajeev |author1link = Rajeev Alur|last2=Henzinger |first2=Thomas A. |author2link = Thomas Henzinger|title=A really temporal logic|journal=[[Journal of the ACM]]|date=Jan 1994 |volume=41 |issue =1|pages=181–203 |doi=10.1145/174644.174651|doi-access=free }}</ref>

== ModelModels ==

Let <math>T\subseteq\mathbb R_+</math>, itwhich intuitively represents a set of timetimes. Let <math>\gamma: T\to \mathcal P(AP)</math> a function whichthat associateassociates to each moment <math>t\in T</math> a set of propositions from ''AP''. A model of a TPTL formula is such a function <math>\gamma</math>. Usually, <math>\gamma</math> is either a [[timed word]] or a [[signal (model checking)|signal]]. In those cases, <math>T</math> is either a discrete subset or an interval containing 0.

== SemanticSemantics ==

Let <math>T</math> and <math>\gamma</math> be as above. Let <math>X</math> be a set of [[clock (model checking)|clocks]]. Let <math>\nu:X\to\mathbb R_{\ge0}</math> (a ''clock valuation'' over <math>X</math>).

We are now going to explain what it means thatfor a TPTL formula <math>\phi</math> holdsto hold at time <math>t</math> for a valuation <math>\nu</math>. This is denoted by <math>\gamma,t,\nu\models\phi</math>.

Let <math>\phi</math> and <math>\psi</math> be two formulas over the set of clocks <math>X</math>, <math>\xi</math> a formula over the set of clocks <math>X\cup\{y\}</math>, <math>x\in X</math>, <math>l\in\mathtt{AP}</math>, <math>c</math> a number and <math>\sim</math> being a comparison operator such as &lt;, &le;, =, &ge; or &gt;:

We first consider formulas whose main operator also belongs to LTL:

* <math>\gamma,t,\nu\models l</math> holds if <math>l\in\gamma(t)</math>,

* <math>\gamma,t,\nu\models\neg\phi</math> holds if either <math>\gamma,t,\nu\not\models\phi</math> or <math>\gamma,t,\nu\models\psi</math>

* <math>\gamma,t,\nu\models\phi\lor\psi</math> holds if either <math>\gamma,t,\nu\models\phi</math> or <math>\gamma,t,\nu\models\psi</math>

* <math>\gamma,t,\nu\models\phi\mathbin\mathcal U\psi</math> holds if there exists <math>t<t''</math> such that <math>\gamma,t'',\nu\models\psi</math> and such that for each <math>t< t'< t''</math>, <math>\gamma,t',\nu\models\phi</math>,

* <math>\gamma,t,\nu\models\phi\mathbin\mathcal S\psi</math> holds if there exists <math>t''< t</math> such that <math>\gamma,t'',\nu\models\psi</math> and such that for each <math>t''<t'<t</math>, <math>\gamma,t',\nu\models\phi</math>,

* <math>\gamma,t,\nu\models y.x\xisim c</math> holds if <math>\gamma,t,-\nu[(y)\tosim t]\models\phic</math> holds,

* <math>\gamma,t,\nu\models xy.\sim cxi</math> holds if <math>\gamma,t-,\nu([y)\simto ct]\models\phi</math> holds.

== Metric temporal logic ==

[[Metric temporal logic]] is another extension of LTL whichthat allowallows tomeasurement measureof 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 semanticsemantics of the formula <math>\phi \mathbin\mathcal {U_I}\psi</math> at some time <math>t</math> is essentially the same than the semanticsemantics 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"/>

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.