AGV 6.1 -- Linear-Time Temporal Logic (LTL)

Notes > UdS AGV

Created At : 2024-11-23 13:40

Count:1.2k Views :

Introduction
Linear-Time Temporal Logic (LTL)
1. Syntax of LTL
2. Remarks
Sematics of LTL
Summary

Previous chapter: Complement Büchi Automaton with Odd Ranking

This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner

Introduction

In the following sections, we introduce several logics for the specification of sets of infinite sequences: LTL, QPTL, and S1S, which can be used to describe $\omega$-regular languages: we can translate a given formula into an automaton that recongnizes the models of the formula.

As a result, we can use the automata-theoretic machinery to answer logical questions like satisfiability or validity. We can also use the logics as a much more convenient starting point, compared to a direct specification using automata, for verification and synthesis.

Linear-Time Temporal Logic (LTL)

Linear-time temporal logic (LTL) is a popular logic for the specification of reactive systems. For a given set of atomic propositions$(AP)$, the formulas of LTL define sets of infinite words over the alphabet $2^{AP}$.

Atomic Propositions:
the interface of a system or a component, such as (a boolean representation of) input and output variables
Words defined by the Formula:
the executions of the system that are considered correct (see example in section 1.1).

Syntax of LTL

φ has to be true until and including the point where ψ first becomes true; if ψ never becomes true, φ must remain true forever.

LTL formulars are constructed from proposition logic with extra temporal operators.

$\begin{array}{lrl} \ \textit{Propositional logic}\newline\hspace{1cm} \cdot \ p,\varphi,\dots\in AP&& \ \text{(Atomic Propositions)}\newline\hspace{1cm} \cdot \ \neg\varphi,\varphi\wedge\psi,\dots&& \ \text{(Logical Operators)}\newline \ \textit{Temporal Operator}\newline\hspace{1cm} \cdot \bigcirc\varphi \ /\ \mathcal{X}\ \varphi& \ \text{Ne}\textbf{X}\text{t: }&\varphi\text{ has to be }\textit{true}\text{ in next state}\newline\hspace{1cm} \cdot \ \Diamond \ \varphi \ /\ \mathcal{F}\ \varphi& \ \textbf{F}\text{inally: }&\varphi\text{ has to be }\textit{true}\text{ eventually}\newline\hspace{1cm} \cdot \ \square \ \varphi \ /\ \mathcal{G}\ \varphi& \ \textbf{G}\text{lobally: }&\varphi\text{ has to be }\textit{true}\text{ for now and so on}\newline\hspace{1cm} \cdot \ \varphi \ \mathcal{U} \ \psi& \ \textbf{U}\text{ntil: }&\varphi\text{ has to be }\textit{true}\textit{ at least }\text{until }\psi\text{ becomes }\textit{true}\newline\hspace{1cm} \cdot \ \varphi \ \mathcal{R} \ \psi& \ \textbf{R}\text{elease: }&\psi\text{ has to be }\textit{true}\text{ until }\varphi\text{ becomes true (inclusive)}\newline&&\psi\text{ remains }\textit{true}\textit{ forever}\text{ if } \varphi\text{ never becomes }\textit{true}\newline\hspace{1cm} \cdot \ \varphi \ \mathcal{W} \ \psi& \ \textbf{W}\text{eak until: }&\varphi\text{ has to be }\textit{true}\textit{ at least }\text{until }\psi\text{ becomes }\textit{true}\text{, or}\newline&&\varphi\text{ remains }\textit{true}\textit{ forever}\text{ if }\psi\text{ never becomes }\textit{true}\newline\hspace{1cm} \cdot \ \varphi \ \mathcal{M} \ \psi& \ \textbf{M}\text{ighty Release: }&\psi\text{ has to be }\textit{true}\text{ until }\varphi\text{ becomes true (inclusive)}\end{array}$

Remarks

When we determine whether a LTL formula is $\textit{true}$ or $\textit{false}$, it only depends on current and future states.

For example, the formula $\varphi\ \mathcal{U}\ \psi$ states that $\varphi$ must remain $\textit{true}$ UNTIL $\psi$ become $\textit{true}$. If the current state we have only $\psi=\textit{true}$, this formula is still evaluated as $\textit{true}$, even if $\varphi$ never become $\textit{true}$.

We can conclude that, $\varphi\ \mathcal{U}\ \psi = \textit{true}$ if:

In current state $\psi$ becomes $\textit{true}$ (regardless of $\varphi$’s condition)
Eventually $\psi$ becomes $\textit{true}$ in certain state (not now), and from now Until that state, $\varphi$ must remain $\textit{true}$

Sematics of LTL

Additional operators

$\mathcal{R}$, $\Diamond\ (\mathcal{F})$, $\square\ (\mathcal{G})$ are considered as additional operators, which can be defined by other LTL operators:

$\varphi\ \mathcal{R}\ \psi\equiv\neg(\neg\varphi\ \mathcal{U}\ \neg\psi)$
$\square\ \varphi \equiv\neg\ \Diamond\ \neg\ \varphi\equiv\ \textit{false}\ \mathcal{R}\ \varphi$
$\Diamond\ \varphi\equiv\textit{true} \ \mathcal{U}\ \varphi$

Weak until $\mathcal{W}$ and Mighty release $\mathcal{M}$

Weak Until is Until that accepts no stop conditions Forever, or Release that include itself as the stop conditions:

$\varphi\ \mathcal{W}\ \psi\equiv(\varphi\ \mathcal{U}\ \psi) \vee \square\ \psi\equiv\psi\ \mathcal{R}\ (\psi\vee\varphi)$

Mighty release is forced to Release Finally, or simply Until both propositions becomes $\textit{true}$:

$\varphi\ \mathcal{W}\ \psi\equiv(\varphi\ \mathcal{R}\ \psi) \wedge \Diamond\ \varphi\equiv\psi\ \mathcal{U}\ (\psi\wedge\varphi)$

Distributivity

$\bigcirc\ (\mathcal{X})$, $\Diamond\ (\mathcal{F})$, $\square\ (\mathcal{G})$, $\mathcal{U}$ satisfied distributivity:

$\bigcirc(\varphi\vee\psi)\equiv(\bigcirc\varphi)\vee(\bigcirc\psi)$
$\bigcirc(\varphi\wedge\psi)\equiv(\bigcirc\varphi)\wedge(\bigcirc\psi)$
$\Diamond(\varphi\vee\psi)\equiv(\Diamond\varphi)\vee(\Diamond\psi)$
$\square(\varphi\wedge\psi)\equiv(\square\varphi)\wedge(\square\psi)$
$\rho\ \mathcal{U}\ (\varphi\vee\psi)\equiv(\rho\ \mathcal{U}\ \varphi)\vee(\rho\ \mathcal{U}\ \psi)$
$(\varphi\wedge\psi)\ \mathcal{U}\ \rho\equiv(\varphi\ \mathcal{U}\ \rho)\wedge(\psi\ \mathcal{U}\ \rho)$
$\bigcirc(\varphi\ \mathcal{U}\ \psi)\equiv(\bigcirc\varphi)\ \mathcal{U}\ (\bigcirc\psi)$

Negation Dual

First of all, NeXt is a self dual:
$\neg\bigcirc\varphi\equiv\bigcirc\neg\varphi$ (Not in next step = Next step won’t happened)
Finally and Globally are dual:
$\neg\Diamond\varphi\equiv\square\neg\varphi$ (Never happened eventually = Forever never happened)
$\neg\square\varphi\equiv\Diamond\neg\varphi$ (Won’t happen forever = eventually won’t happen anymore)
Until and Release are dual:
$\neg(\varphi\ \mathcal{U}\ \psi)\equiv\neg\varphi\ \mathcal{R}\ \neg\psi$ ($\psi$ won’t happen until $\varphi$ stops = $\psi$ can’t happen unless $\varphi$ stops)
$\neg(\varphi\ \mathcal{R}\ \psi)\equiv\neg\varphi\ \mathcal{U}\ \neg\psi$ (Never stop $\psi$ with $\varphi$ = $\varphi$ never happens, if it does, that means $\psi$ has been stopped)
Similarly, Weak Until and Mighty Release are also dual:
$\neg(\varphi\ \mathcal{W}\ \psi)\equiv\neg\varphi\ \mathcal{M}\ \neg\psi$
$\neg(\varphi\ \mathcal{M}\ \psi)\equiv\neg\varphi\ \mathcal{W}\ \neg\psi$

Special temporal properties

$\Diamond\varphi\equiv\Diamond\Diamond\varphi$
(Finally Finally $\varphi$ is $\textit{true}$)
$\square\varphi\equiv\square\square\varphi$
($\varphi$ is always always $\textit{true}$)
$\varphi\ \mathcal{U}\ \psi\equiv\varphi\ \mathcal{U}\ (\varphi\ \mathcal{U}\ \psi)$
($\varphi$ is $\textit{true}$ Until $\psi$ become $\textit{true}$ = $\varphi$ is $\textit{true}$ Until, if “$\varphi$ is $\textit{true}$ Until $\psi$ become $\textit{true}$” is $\textit{true}$)
$\Diamond\varphi\equiv\varphi\vee \bigcirc(\Diamond\varphi)$
( $\varphi$ Finally becomes $\textit{true}$ = either now $\varphi$ is $\textit{true}$ or in neXt step $\varphi$ Finally becomes $\textit{true}$)
$\square\varphi\equiv\varphi\wedge \bigcirc(\square\varphi)$
( $\varphi$ is always $\textit{true}$ = now $\varphi$ is $\textit{true}$ and in neXt step $\varphi$ is also always $\textit{true}$)

Summary

In this section, we have go through basic sytanx and properties of LTL. In next section we will try to apply the formula to some systems and $\omega$-languages.

Next chapter: Expressing Program Properties using LTL