Past Time Linear Temporal Logic

From FSL
Jump to: navigation, search

Past time Linear Temporal Logic (ptLTL) is a logic for specifying properties of reactive and concurrent systems. ptLTL provides temporal operators that refer to the past states of an execution trace relative to a current point of reference. The logic plugin here is based on an rewriting-based algorithm for generating an optimized monitoring program from an ptLTL formula.

The PTLTL formula follows the following syntax:

<Fm> ::= true | false | A | ! <Fm> | <Fm> /\ <Fm> | <Fm> \/ <Fm> | <Fm> ++ <Fm> | <Fm> -> <Fm> | <Fm> <-> <Fm> | [*] <Fm> | <*> <Fm> | (*) <Fm> | <Fm> Ss <Fm> | <Fm> Sw <Fm> | [ <Fm> , <Fm> )s | [ <Fm> , <Fm> )w | start(<Fm>) | end(<Fm>)

The different operators in decreasing order of precedence are [*], <*>, (*) > ! > U > /\ > ++ > \/ > -> > <-> > Ss, Sw. A is an event or a predicate. The propositional binary operators, e.g. /\, ++ and so on, are the standard ones, that is, disjunction, conjunction, implication, equivalence, and exclusive disjunction (++).

The standard past time and the monitoring operators are called ``temporal operators, because they refer to other (past) moments in time. The operator (*) F should be read ``previously F; its intuition is that F held at the immediately previous step of execution. <*> F should be read ``eventually in the past F, with the intuition that there is some past moment in time when F was true. [*] F should be read ``always in the past f, with the obvious meaning. The operator F1 Ss F2, which should be read ``F1 strong since F2, reflects the intuition that F2 held at some moment in the past and, since then, F1 held all the time. F1 Sw F2 is a weak version of ``since, read ``F1 weak since F2, saying that either F1 was true all the time or otherwise F1 Ss F2. The monitoring operators start, end, [ )s, and [ )w were inspired by work in runtime verification. We found these operators often more intuitive and compact than the usual past time operators in specifying runtime requirements, despite the fact that they have the same expressive power as the standard ones. The operator start(F) should be read ``start F; it says that the formula F just started to be true, that is, it was false previously but it is true now. Dually, the operator end(F) which is read ``end F, carries the intuition that F ends to be true, that is, it was previously true but it is false now. The operators [F1,F2)s and [F1,F2)w are read ``strong/weak interval F1,F2 and they carry the intuition that F1 was true at some point in the past but F2 has not been seen to be true since then, including that moment.

Example: [*](start(dialing) -> !((*)(busyTone\/connected))) (one cannot dial when the phone is busy or connected)

Online Demo Back to logic repository

Personal tools