Linear temporal logic

Linear temporal logic ( LTL or Linear temporal logic ) is a formal modal temporal logic that is set up and used for model testing. In LTL formulas about the future of paths are set up, for example, that a condition eventually becomes true or a condition remains true until another condition is fulfilled.

syntax

LTL is made up of a set of statement variables , the logical links and the following temporal modal operators: ${\displaystyle p_{1},p_{2},...}$ ${\displaystyle \neg ,\lor ,\land ,\rightarrow }$

• X for successor (ne x t; N is used synonymously)
• G for g lobal
• F for sometime ( f inally)
• U for to ( u ntil)
• R for r elease.

The first three operators are unary , so X is a syntactically correct formula if it is syntactically correct. The last two operators are binary, so U is a syntactically correct formula if and are syntactically correct formulas. ${\displaystyle \phi }$ ${\displaystyle \phi }$ ${\displaystyle \phi }$ ${\displaystyle \psi }$ ${\displaystyle \phi }$ ${\displaystyle \psi }$

semantics

An LTL formula can be evaluated over an infinite sequence of statements as well as a single position on the path. An LTL formula is fulfilled on a path if and only if it is fulfilled in position 0 of the path. The semantics of the modal operators are as follows.

Text form	symbol	Explanation	Sample path
One-digit links :
X ${\displaystyle \phi }$	${\displaystyle \circ \phi }$	next (Ne X t): applies to the next state. ${\displaystyle \phi }$
G ${\displaystyle \phi }$	${\displaystyle \Box \phi }$	G lobal: applies to the entire subsequent path. ${\displaystyle \phi }$
F. ${\displaystyle \phi }$	${\displaystyle \Diamond \phi }$	F inally: applies sometime on the following path. ${\displaystyle \phi }$
Two-digit links :
${\displaystyle \psi }$ U ${\displaystyle \phi }$	${\displaystyle \psi {\mathcal {U}}\phi }$	U ntil: applies to the current or a subsequent position and applies at least until this position is reached. In this position no longer has to apply. ${\displaystyle \phi }$ ${\displaystyle \psi }$ ${\displaystyle \psi }$
${\displaystyle \psi }$ R. ${\displaystyle \phi }$	${\displaystyle \psi {\mathcal {R}}\phi }$	R elease: applies up to and including the first position at which applies, or forever if such a position does not exist. ${\displaystyle \phi }$ ${\displaystyle \psi }$

Two of the operators are already fundamental, that is, they define the others using suitable links:

• F = true U ${\displaystyle \phi }$ ${\displaystyle \phi }$
• G = false R = F ${\displaystyle \phi }$ ${\displaystyle \phi }$ ${\displaystyle \neg }$ ${\displaystyle \neg }$ ${\displaystyle \phi }$
• ${\displaystyle \psi }$ R = ( U ) ${\displaystyle \phi }$ ${\displaystyle \neg }$ ${\displaystyle \neg }$ ${\displaystyle \psi }$ ${\displaystyle \neg }$ ${\displaystyle \phi }$

Special links

Some authors define a weak-to-operator ( weak until , with W hereinafter) of as having a similar semantics to operator, however, no holding condition is required. Sometimes it makes sense if U and R can be defined using formulas of the weak to operator:

• ${\displaystyle \psi }$ U = F ( W ) ${\displaystyle \phi }$ ${\displaystyle \phi }$ ${\displaystyle \land }$ ${\displaystyle \psi }$ ${\displaystyle \phi }$
• ${\displaystyle \psi }$ R = W ( ) ${\displaystyle \phi }$ ${\displaystyle \phi }$ ${\displaystyle \psi }$ ${\displaystyle \land }$ ${\displaystyle \phi }$
• ${\displaystyle \phi }$ W = R ( ) ${\displaystyle \psi }$ ${\displaystyle \psi }$ ${\displaystyle \psi }$ ${\displaystyle \lor }$ ${\displaystyle \phi }$
• ${\displaystyle \phi }$ W = ( U ) G ${\displaystyle \psi }$ ${\displaystyle \phi }$ ${\displaystyle \psi }$ ${\displaystyle \lor }$ ${\displaystyle \phi }$

Important properties

There are two major classes of properties that can be described by linear temporal logic: security ( safety ), indicates that something undesirable never occurs ( G ) and vitality ( liveness ), which says that something Erwünschtes happens all the time ( GF or G F ). In general: Security properties are those for which a finite prefix is ​​sufficient as a counterexample , the infinite extension of which always violates the property. In the case of liveliness properties, any finite prefix of a path can be extended to an infinite path that satisfies the formula. ${\displaystyle \neg }$ ${\displaystyle \phi }$ ${\displaystyle \psi }$ ${\displaystyle (\phi \rightarrow }$ ${\displaystyle \psi )}$

Equivalent transformations

The following equivalent transformations are possible:

${\displaystyle X(\phi \lor \psi )\equiv X\phi \lor X\psi }$

${\displaystyle X(\phi \land \psi )\equiv X\phi \land X\psi }$

${\displaystyle X\neg \phi \equiv \neg X\phi }$

${\displaystyle X(\phi U\psi )\equiv (X\phi )U(X\psi )}$

${\displaystyle F(\phi \lor \psi )\equiv F\phi \lor F\psi }$

${\displaystyle \neg F\phi \equiv G\neg \phi }$

${\displaystyle G(\phi \land \psi )\equiv G\phi \land G\psi }$

${\displaystyle \neg G\phi \equiv F\neg \phi }$

${\displaystyle (\phi \land \psi )U\rho \equiv (\phi U\rho )\land (\psi U\rho )}$

${\displaystyle \rho U(\phi \lor \psi )\equiv (\rho U\phi )\lor (\rho U\psi )}$

${\displaystyle F\phi \equiv FF\phi }$

${\displaystyle G\phi \equiv GG\phi }$

${\displaystyle \phi U\psi \equiv \phi U(\phi U\psi )}$

${\displaystyle F\phi \equiv \phi \lor XF\phi }$

${\displaystyle G\phi \equiv \phi \land XG\phi }$

${\displaystyle \phi U\psi \equiv \psi \lor (\phi \land X(\phi U\psi ))}$

${\displaystyle \phi W\psi \equiv \psi \lor (\phi \land X(\phi W\psi ))}$

${\displaystyle \phi R\psi \equiv (\phi \land \psi )\lor (\psi \land X(\phi R\psi ))}$

Relationships with other logics

Linear temporal logic (LTL) is a subset of Computation Tree Logic * (CTL *), has a common subset with CTL , but is neither a superset nor a subset of CTL.

LTL is equivalent to predicate logic with single-digit relation symbols and the smaller relation , as well as asterisk -free regular expressions . ${\displaystyle (P_{i})_{i\geq 1}}$ ${\displaystyle {\text{FO}}[<,(P_{i})_{i\geq 1}]}$

Automata-theoretical LTL model checking

An important way to validate the model is to express the desired properties (as described above) using LTL operators and then verify that the model meets those properties.

It is also possible to create a Büchi automaton that is equivalent to the model and one that is equivalent to negating the property to be tested. The intersection of the two non-deterministic Büchi automata is empty if the model fulfills the properties.

See also

• Computation Tree Logic (CTL)

Web links

Commons : Linear Temporal Logic  - collection of images, videos and audio files

• P. Gumm - Linear Temporal Logic from the University of Marburg (PDF, 3.12 MB)
• A presentation of LTL (English, PDF, 90 kB)
• Linear-Time Temporal Logic and Büchi Automata (English, PDF, 212 kB)