Timed propositional temporal logic: Difference between revisions

Revision as of 19:01, 6 February 2025

Latest revision as of 19:48, 6 February 2025

(5 intermediate revisions by one other user 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> 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 book |last1=Bouyer |first1=Patricia |author1-link=Patricia Bouyer-Decitre|last2=Chevalier |first2=Fabrice |last3=Markey |first3=Nicolas |title=FSTTCS 2005: Foundations of Software Technology and Theoretical 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}}

== Models ==

Line 29:

* <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 <math>\gamma,t,\nu\not\models\phi</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 x\sim c</math> holds if <math>t-\nu(y)\sim c</math>,{{clarify|reason='y' should be 'x'?|date=February 2025}}

* <math>\gamma,t,\nu\models y.\xi</math> holds if <math>\gamma,t,\nu[y\to t]\models\phi</math> holds.{{clarify|reason='\phi' should be '\xi'?|date=February 2025}}

== 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"/>