Timed propositional temporal logic: Difference between revisions

Revision as of 05:39, 22 March 2019

Latest revision as of 19:48, 6 February 2025

(22 intermediate revisions by 14 users not shown)

Line 1:

In [[model checking]], a field of [[computer science]], '''Timedtimed Propositionalpropositional Temporaltemporal Logiclogic''' ('''TPTL''') is an extension of propositional [[Linearlinear Temporaltemporal Logiclogic]] (LTL) in wichwhich variables are introduced to measure times between two events. For example, while LTL allows to state that each event ''p'' is eventually followed by an event ''q'', TPTL furthermore allows to give a time limit for ''q'' to occur.

== 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=roceedingsProceedings of the 25th Conference on Foundations of Software Technology and Theoretical Computer SciencScience |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 opeartoroperator '''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 (JACM]]|date=Jan 1994 |volume=41 |issue =1|pagepages=181-203181–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}}

== Model ==

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

LetWe <math>T</math>are andnow going to explain what it means for a TPTL formula <math>\gammaphi</math> asto above.hold at Lettime <math>Xt</math> for a set of [[clock (model checking)|clocks]]. Letvaluation <math>\nu:X\to\mathbb R_{\ge0}</math>. aThis clockis valuationdenoted overby <math>X\gamma,t,\nu\models\phi</math>.

We are now going to explain what it means that a TPTL formula <math>\phi</math> holds 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>.

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

== From Metric Temporal Logic to TPTL ==

[[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>.

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.

The MTL formula <math>\phi\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"/>

TPTL is strictly more expressive than MTL{{r|ExpressivenesOfTPTLAndMtl|p=2}} both over timed words and over signals. Over timed words, no MTL formula is equivalent to <math>\Box(a\implies x.\Diamond(b\land\Diamond(c\land x\le 5)))</math>. Over signal, there are no MTL formula equivalent to <math>x.\Diamond(a\land x\le 1\land\Box(x\le 1\implies\neg b))</math>, which states that the last atomic proposition before time point 1 is an <math>a</math>.

It follows that any other operator introduced in the page [[metric temporal logic#Operators defined from MTL operator]] can also be defined as TPTL formulas.

== Comparison with LTL ==