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

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}{l}\mathit{\text{Propositional logic}}\\ \cdot p,\phi ,\cdots \in AP& & \text{(Atomic Propositions)}\\ \cdot \mathrm{\neg }\phi ,\phi \wedge \psi ,\dots & & \text{(Logical Operators)}\\ \mathit{\text{Temporal Operator}}\\ \cdot ◯\phi /\mathcal{X}\phi & \text{Ne}\mathbf{\text{X}}\text{t: }& \phi \text{ has to be }\mathit{\text{true}}\text{ in next state}\\ \cdot ◊\phi /\mathcal{F}\phi & \mathbf{\text{F}}\text{inally: }& \phi \text{ has to be }\mathit{\text{true}}\text{ eventually}\\ \cdot ◻\phi /\mathcal{G}\phi & \mathbf{\text{G}}\text{lobally: }& \phi \text{ has to be }\mathit{\text{true}}\text{ for now and so on}\\ \cdot \phi \mathcal{U}\psi & \mathbf{\text{U}}\text{ntil: }& \phi \text{ has to be }\mathit{\text{true}}\mathit{\text{ at least }}\text{until }\psi \text{ becomes }\mathit{\text{true}}\\ \cdot \phi \mathcal{R}\psi & \mathbf{\text{R}}\text{elease: }& \psi \text{ has to be }\mathit{\text{true}}\text{ until }\phi \text{ becomes true (inclusive)}\\ & & \psi \text{ remains }\mathit{\text{true}}\mathit{\text{ forever}}\text{ if }\phi \text{ never becomes }\mathit{\text{true}}\\ \cdot \phi \mathcal{W}\psi & \mathbf{\text{W}}\text{eak until: }& \phi \text{ has to be }\mathit{\text{true}}\mathit{\text{ at least }}\text{until }\psi \text{ becomes }\mathit{\text{true}}\text{, or}\\ & & \phi \text{ remains }\mathit{\text{true}}\mathit{\text{ forever}}\text{ if }\psi \text{ never becomes }\mathit{\text{true}}\\ \cdot \phi \mathcal{M}\psi & \mathbf{\text{M}}\text{ighty Release: }& \psi \text{ has to be }\mathit{\text{true}}\text{ until }\phi \text{ becomes true (inclusive)}\end{array}$

Remarks

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

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

We can conclude that, $\phi \mathcal{U}\psi =\mathit{\text{true}}$ if:

1. In current state $\psi$ becomes $\mathit{\text{true}}$ (regardless of $\phi$’s condition)
2. Eventually $\psi$ becomes $\mathit{\text{true}}$ in certain state (not now), and from now Until that state, $\phi$ must remain $\mathit{\text{true}}$

Sematics of LTL

Additional operators

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

• $\phi \mathcal{R}\psi \equiv \mathrm{\neg }(\mathrm{\neg }\phi \mathcal{U}\mathrm{\neg }\psi )$
• $◻\phi \equiv \mathrm{\neg }◊\mathrm{\neg }\phi \equiv \mathit{\text{false}}\mathcal{R}\phi$
• $◊\phi \equiv \mathit{\text{true}}\mathcal{U}\phi$

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:

• $\phi \mathcal{W}\psi \equiv (\phi \mathcal{U}\psi )\vee ◻\psi \equiv \psi \mathcal{R}(\psi \vee \phi )$

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

• $\phi \mathcal{W}\psi \equiv (\phi \mathcal{R}\psi )\wedge ◊\phi \equiv \psi \mathcal{U}(\psi \wedge \phi )$

Distributivity

$◯(\mathcal{X})$, $◊(\mathcal{F})$, $◻(\mathcal{G})$, $\mathcal{U}$ satisfied distributivity:

• $◯(\phi \vee \psi )\equiv (◯\phi )\vee (◯\psi )$
• $◯(\phi \wedge \psi )\equiv (◯\phi )\wedge (◯\psi )$
• $◊(\phi \vee \psi )\equiv (◊\phi )\vee (◊\psi )$
• $◻(\phi \wedge \psi )\equiv (◻\phi )\wedge (◻\psi )$
• $\rho \mathcal{U}(\phi \vee \psi )\equiv (\rho \mathcal{U}\phi )\vee (\rho \mathcal{U}\psi )$
• $(\phi \wedge \psi )\mathcal{U}\rho \equiv (\phi \mathcal{U}\rho )\wedge (\psi \mathcal{U}\rho )$
• $◯(\phi \mathcal{U}\psi )\equiv (◯\phi )\mathcal{U}(◯\psi )$

Negation Dual

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

Special temporal properties

• $◊\phi \equiv ◊◊\phi$
  (Finally Finally $\phi$ is $\mathit{\text{true}}$)
• $◻\phi \equiv ◻◻\phi$
  ($\phi$ is always always $\mathit{\text{true}}$)
• $\phi \mathcal{U}\psi \equiv \phi \mathcal{U}(\phi \mathcal{U}\psi )$
  ($\phi$ is $\mathit{\text{true}}$ Until $\psi$ become $\mathit{\text{true}}$ = $\phi$ is $\mathit{\text{true}}$ Until, if “$\phi$ is $\mathit{\text{true}}$ Until $\psi$ become $\mathit{\text{true}}$” is $\mathit{\text{true}}$)
• $◊\phi \equiv \phi \vee ◯(◊\phi )$
  ( $\phi$ Finally becomes $\mathit{\text{true}}$ = either now $\phi$ is $\mathit{\text{true}}$ or in neXt step $\phi$ Finally becomes $\mathit{\text{true}}$)
• $◻\phi \equiv \phi \wedge ◯(◻\phi )$
  ( $\phi$ is always $\mathit{\text{true}}$ = now $\phi$ is $\mathit{\text{true}}$ and in neXt step $\phi$ is also always $\mathit{\text{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

Further Reading: