# Specifications in Linear-time Temporal Logic (LTL)

Our goal is to specify the properties that a model must fulfill in order to be correct. A model in our setting is a transition systems that represents a potentially infinite set of executions, that are themselves potentially infinite. So, a specification should describe the set of correct executions. Then, a verification algorithm will check that all the executions of the model belong to the set of correct executions.

## Atomic propositions

A specification is the set of expected behaviors (or runs) of a model. Consider the abstract model of a drink vendor machine below.

• A path is a sequence of states in the model which are related by transitions. For instance `coke pay select sprite` is a path, since `coke -> pay`, `pay ->select` and `select -> sprite` are transitions.
• A run is a path starting from an initial state of the model. For instance `pay select coke pay select coke` is a run since it is a path (successive states are connected by transitions) that starts from initial state `pay`.
• A trace is the sequence of labels observed along a path (or a run). For instance `{pay} {} {drink} {pay} {} {drink}` is the trace of the run `pay select coke pay select coke`. It is also the trace of the run `pay select sprite pay select coke`.

The labels on states are called atomic propositions. Notice that states are labelled by sets of atomic propositions. Hence, a trace is a sequence (or word) of sets of atomic propositions. For instance, in the word `{pay} {} {drink} {pay} {} {drink}`, the letters are sets of atomic propositions `{pay}`, `{drink}` and `{}`.

In the sequel, we only consider infinite runs and traces.

1. We want to express the fact that “every paid drink is eventually served”. Express this requirement as a property of run, then as a property of traces.
2. Assume that we add a third drink “Orange juice”, what happens to your properties? What is the goal of labeling states with atomic propositions?
3. Express the requirement “there is no free drink” as a property of traces

## Linear Temporal Logic (LTL)

LTL is a formal language to describe sets of infinite traces. We use it to specify the expected traces of a model.

Formulas in LTL are built from atomic propositions, boolean operators (and, or, not, implies, iff) and temporal modalities that we describe below.

### Always and Eventually

• `[]` (or `G`) always, that expresses that some formula is true for every position in a trace.
• `<>` (or `F`) eventually, that tells that some formula is true in at least one position in a trace.

Consider again the model of the drink vendor machine above. - an infinite run in this model satisfies the property `[] pay` if every state on the run has (at least) label `pay`. Observe that there is no such run in the model. - an infinite run satisfies `<> drink` if there is a state on the run that has (at least) label `drink`. Observe that every run satisfies this property since its third state is either `coke` or `sprite` which are both labeled `{drink}`.

Formally, out set of formulas is defined as:

• `p` is a formula for every atomic proposition `p`
• and for any two LTL formulas `f1` and `f2`, `f1 /\ f2`, `f1 \/ f2`, `~f1`, `f1 => f2`, `f1 <=> f2`, `[] f1` and `<> f1` are LTL formulas

So `pay` is a formula, as well as `pay \/ drink`, `[] (pay => drink)` and `<> (drink => [] pay)`.

Given an infinite trace `l = l1 l2 ... li ...`, the satisfaction relation is defined by (recall that `li` is a set of atomic propositions):

• for atomic proposition `p`, `l |= p` if `l1` contains `p`
• `l |= f1 /\ f2` if `l |= f1` and `l |= f2` (and similarly for `\/`, `=>` and `<=>`)
• `l |= ~f` if not `l |= f`
• `l |= [] f` if for all `j >= 1`, `lj ... |= f`
• and `l |= <> f` if there exists `j >= 1` such that `lj ... |= f`.

Finally, a transition system `S` satisfies an LTL formula `f` if every trace of `S` satisfies `f`.

First, express in french the following LTL formulas. Then, tell which formulas are true for the transition system below where states are of the form `(pc,x)`.

1. `<> (pc = "Done")`
2. `[] (-2 <= x /\ x <= 2)`
3. `<> (pc="Done") \/ [] (x <= 0)`
4. `[] (pc="l1" => x > -2)`
5. `[]<> x=0`
6. `<>[] x=0`
7. `<> (pc="Done") => <>[] (pc="Done")`

### Limits of Always and Eventually

Consider again the abstract model of a drink vendor machine above. We want to check that the following two requirements hold:

• Every paid drink is eventually served
• There is no free drink
1. Explain why the LTL formula `[] (pay => <> drink)` fails to express the first requirement.
2. Give a transition system that satisfies the formula `[] (pay => <> drink)` but that does guarantee that “every paid drink is eventually served”

### Until and Next

We introduce two new modalities:

• `X`, next, and let `X f` be an LTL formula if `f` is an LTL formula,
• and `U`, until, and we accept `f1 U f2` as an LTL formula if `f1` and `f2` are LTL formulas.

The meaning of `X f` is that `f` must hold in the next position of the trace. The meaning of `f1 U f2` is that `f2` must hold at some point on the trace, and in the mean time, `f1` must be true.

Formally, for an infinite trace `l= l1 l2 ... li ...`

• `l |= X f` if `l2 ... |= f`

• `l |= f1 U f2` if there exists a `j >= 1` such that `lj ... |= f2` and for every intermediate position `1 <= i < j`, `li ... |= f1`.

So for instance, `a U b` means that `b` should be true at some point (now or in the future), and, meanwhile, `a` must hold, and `X a` means that a must hold from the second position of the trace.

1. Using the transition system corresponding to the small program above, tell which of the following formula are satisfied:

1. `(x >= 0) U (pc="Done")`
2. `(x > 10) U (pc="l0")`
3. `X (x > -2)`
2. Express `<>` using `U`. Then, express `[]` using `<>`.

3. Express the two requirements above on the drink vendor machine in LTL.