Timed propositional temporal logic: Difference between revisions

Revision as of 13:42, 13 June 2023

Latest revision as of 19:48, 6 February 2025

(8 intermediate revisions by 3 users not shown)

Line 2:

== Syntax ==

The '''future fragment of TPTL''' is defined similarly to [[linear temporal logic]], in which furthermore, [[clock (model checking)|clock]] variables can be introduced and compared to constants. Formally, given a set <math>X</math> of clocks, {{clarify span|MTL|reason=Should be 'TPTL'? MTL is discussed in a later section.|date=February 2025}} is built up from:

* a finite set of [[propositional variable]]s ''AP'',

* 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;.{{clarify|reason=Since the set of logical connectives is chosen minimal (without e.g. \lor), the same could be done here. If times are ordered totally, \leq would be sufficient.|date=February 2025}}

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

Furthermore, for <math>I=(a,b)</math> an interval, <math>x\in I</math> is considered as an abbreviation for <math>x>a\land x<b</math>; and similarly for every other kind of intervals.

The logic '''TPTL+Past'''<ref name="ExpressivenesOfTPTLAndMtl">{{cite journalbook |last1=Bouyer |first1=Patricia |author1-link=Patricia Bouyer-Decitre|last2=Chevalier |first2=Fabrice |last3=Markey |first3=Nicolas |title=OnFSTTCS the2005: ExpressivenessFoundations of TPTLSoftware Technology and MTLTheoretical Computer Science |chapter=Developments in Data Structure Research During the First 25 Years of FSTTCS |series=Lecture Notes in Computer Science |journal=Proceedings of the 25th Conference on Foundations of Software Technology and Theoretical Computer Science |date=2005 |volume=3821 |page=436 |doi=10.1007/11590156_3 |isbn=978-3-540-30495-1 |chapter-url=https://hal.archives-ouvertes.fr/hal-01194615/document}}</ref> is built as the future fragment of {{clarify span|'''TLS'''|reason=Should be introduced or linked.|date=February 2025}} and also contains

* the temporal modal operator '''S'''.

Note that theThe next operator {{clarify span|'''N'''|reason=Introduce or link|date=February 2025}} is not considered to be a part of {{clarify span|MTL|date=February 2025}} 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 |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>{{clarify|reason=The set of clocks of a formula needs to be introduced (I guess along with the syntax case distinction above).|date=February 2025}}

== 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>, or both

* <math>\gamma,t,\nu\models\phi\mathbin\mathcal U\psi</math> holds if there exists <math>t<t''</math> such that <math>t<t''</math> and <math>\gamma,t'',\nu\models\psi</math> and such that for each <math>t'</math> with <math>t< t'< t''</math>, &nbsp; <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>t''< t</math> and <math>\gamma,t'',\nu\models\psi</math> and such that for each <math>t'</math> with <math>t''<t'<t</math>, &nbsp; <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>,{{clarify|reason='y' holds,should be 'x'?|date=February 2025}}

* <math>\gamma,t,\nu\models xy.\sim cxi</math> holds if <math>\gamma,t-,\nu([y)\simto ct]\models\phi</math> holds.{{clarify|reason='\phi' should be '\xi'?|date=February 2025}}

== 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 numbernumbers. 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.