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.

Specifications should be expressed independently of the model to verify. In other words, the same specification can be chcked on different models that should fulfill this specification. For instance, the postcondition of a sorting algorithm expresses that upon termination, the array is sorted. This specification does not depend on the specific algorithm, and any sorting algorithm can be checked against this specification.

The executions of a model consist of state sequences. Obviously, states strongly depends on the model. So expressing specifications in terms of states of the model is **not** independent of a specific model. We need an abstraction that captures the relevant properties of the states, from which we can express the specifications. To that purpose, we label the states of a system with (sets of) **atomic propositions**. These atomic propositions are meant to abstract the states. An execution (sequence of states) is this observed as a sequence of (sets of) atomic propositions. Specifications can thus be expressed as the set of observations that are considered valid.

As an example, consider the abstract model of a drink vendor machine below:

An execution like: `pay select sprite pay select coke pay select coke ...`

is viewed as the sequence of sets of atomic labels: `{pay} {} {drink} {pay} {} {drink} {pay} {} {drink} ...`

. Observe that the kind of drink is abstracted away.

In the example above, atomic propositions are simply labels. For PlusCal models, atomic propositions can be any predicate over the variables in the model. For instance, `pc="Done"`

is an atomic proposition that labels all the states such that the variable `pc`

has value `Done`

, and none of the other states. Similarly `x<=2`

labels all the states in which `x`

have a value less-than-or-equal-to `2`

. A state that has value `Done`

for `pc`

and `2`

for `x`

is labeled by the two atomic propositions. More precisely, its set of labels is `{pc="Done", x<=2}`

. A state with value `Done`

for `pc`

and `5`

for `x`

has label: `{pc="Done"}`

. Finally, a state with value `l0`

for `pc`

and `7`

for `x`

has the empty set `{}`

of labels.

In the sequel, we call **executions** the runs of a model (i.e. paths from an initial state in a transition system), and **traces** the sequences of (sets of) labels.

NB: TLA+ allows atomic propositions over pairs of states (i.e. transitions) in certain circumstances. Except one example in one of the next lectures, we will consider atomic propositions which are state formulas.

The purpose of specification is to define the set of **valid traces**. In order to simplify, we will only consider **infinite traces**, hence infinite executions of transition systems. More precisely, a model may have finite and infinite behaviors. The verification algorithm will consider all the infinite executions, but ignore the finite ones.

Consider the model below that consists of a simple PlusCal algorithm that decrements a variable `x`

until it becomes equal to 0. The variable `x`

is reset to 0 when it becomes too small.

```
EXTENDS Integers, TLC
(* PlusCal options (-termination) *)
(*
--algorithm simple_process {
variables
x \in -2..2;
{
l0: while (x /= 0) {
if (x < -1)
x := 0;
l1: x := (x - 1);
}
}
}
*)
```

- Draw the transition system corresponding to this algorithm. Does it have finite runs? Infinite runs?
- Transform the transition system in such a way that it only has infinite runs. Your transformation should represent the same set of behaviors (except, of course, from the point of view of termination).
- Explain how this transformation is implemented in the translation of the PlusCal algorithm in TLA+.
- Explain how termination can be expressed in this new settings.

Specifications express properties that must be fulfilled by the model. These properties themselves characterize the valid traces: those that match the property. Since specifications characterize infinite traces, we need a language to define the set of valid traces. We will now introduce a such a language, the **Linear Temporal Logic (LTL)**, that allows to reason about traces.

Linear Temporal Logic allows to write formulas that are interpreted as sets of (valid) traces. Formulas in LTL are built from atomic propositions that can be combined using boolean operators (and, or, not, implies, iff) and **temporal modalities**. We first focus on two temporal modalities:

`[]`

(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.

So, a run of a model (with a variable `x`

) will satisfy the formula `[] x <= 2`

if `x`

is less-or-equal to 2 in every state of the run. And, it will satisfy `<> x > 1`

if `x`

is greater that 1 at some point on the run.

Formally, LTL formulas are 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 `pc="Done"`

is a formula, as well as `pc="Done" /\ x<=2`

, `[] (pc="Done" => x <= 2)`

and `[](pc="Done") => <> x <= 2`

.

Given a trace `l = l1 l2 ... li ...`

, the satisfaction relation if defined by:

- 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 specifications. Then, using both the transition system corresponding to the PlusCal algorithm above and the model-checker, tell which ones of the following formulas are satisfied by the PlusCal algorithm:

`<> (pc = "Done")`

`[] (-2 <= x /\ x <= 2)`

`<> (pc="Done") \/ [] (x <= 0)`

`[] (pc="l1" => x > -2)`

`[]<> x=0`

`<>[] x=0`

`<> (pc="Done") => <>[] (pc="Done")`

Consider the abstract drink vendor machine above. We want to verify the following two requirements:

- if one pays, one eventually gets a drink
- if one gets a drink, one has paid for it before

Explain why the LTL formula `[] (pay => <> drink)`

fails to express the first requirement.

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.

Using the transition system corresponding to the PlusCal algorithm above, tell which of the following formula are satisfied:

`(x >= 0) U (pc="Done")`

`(x > 10) U (pc="l0")`

`X (x > -2)`

Express

`<>`

using`U`

. Then, express`[]`

using`<>`

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

Which of the following are true:

`pi |= a U b`

`pi |= <>b => a U b`

`pi |= X X ~b`

`pi |= []a`

`pi |= []<>a`

A transition system `S`

satisfies an LTL formula `f`

if alls its runs satisfy `f`

, denoted `S |= f`

. Let `S`

be the transition system depicted above. Which of the following are true:

`S |= a`

`S |= <>[]a`

`S |= <>[]b \/ []<>(~a /\ ~b)`

`S |= [](a => (X ~a \/ b))`

Finally, find a transition system `S`

and a formula `f`

such that `S`

does not satisfy `f`

and `S`

does not satisfy `~f`

.