Specifications in Linear 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

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:

drink vendor machine

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.

Infinite executions

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);
    }
  }

}
*)
  1. Draw the transition system corresponding to this algorithm. Does it have finite runs? Infinite runs?
  2. 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).
  3. Explain how this transformation is implemented in the translation of the PlusCal algorithm in TLA+.
  4. Explain how termination can be expressed in this new settings.

Always and Eventually

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:

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:

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:

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:

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

Until and Next

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

Explain why the LTL formula [] (pay => <> drink) fails to express the first requirement.

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

Illustration

A transition system

Which of the following are true:

  1. pi |= a U b
  2. pi |= <>b => a U b
  3. pi |= X X ~b
  4. pi |= []a
  5. 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:

  1. S |= a
  2. S |= <>[]a
  3. S |= <>[]b \/ []<>(~a /\ ~b)
  4. 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.