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.