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.

drink vendor machine

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

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:

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):

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")
Program transition system

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:

  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:

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

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.