Timed propositional temporal logic: Difference between revisions

Revision as of 05:39, 22 March 2019

Revision as of 05:39, 22 March 2019

Line 1:

In [[model checking]], a field of [[computer science]], '''Timed Propositional Temporal Logic''' ('''TPTL''') is an extension of [[Linear Temporal Logic]] (LTL) in wich variables are introduced to measure times between two events. For example, Whilewhile 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 ==

Line 43:

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

A standard (untimed) infinite word <math>w=a_0,a_1,\dots,</math> is a function from <math>\mathbb N</math> to <math>A</math>. We can consider such a word using the set of time <math>T=\mathbb N</math>, and the function <math>\gamma(i)=a_i</math>. In this case, for <math>\phi</math> an arbitrary LTL formula, <math>w,i\models\phi</math> if and only if <math>\gamma,i,\nu\models\phi</math>, where <math>\phi</math> is considered as a TPTL formula with non-strict operator, and <math>\nu</math> is the only function defined on the empty set.

==References==