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.

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

- 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.
- Assume that we add a third drink “Orange juice”, what happens to your properties? What is the goal of labeling states with atomic propositions?
- Express the requirement “there is no free drink” as a property of traces

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.

`[]`

(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)`

.

`<> (pc = "Done")`

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

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

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

`[]<> x=0`

`<>[] x=0`

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

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

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

fails to express the first requirement. - Give a transition system that satisfies the formula
`[] (pay => <> drink)`

but that does guarantee that “every paid drink is eventually served”

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 small program 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.