14.2 Temporal Propositions

14.2 Temporal Propositions

Fluents let us express properties about the abstract state of a system at a particular point in time. This state depends on the trace of actions that have occurred up to that point in time. To express propositions with respect to an execution of a model, we need to introduce some temporal operators.

14.2.1 Safety Properties

To illustrate the expression of safety properties using fluents, we return to the mutual exclusion example of section 7.1.2.

 const N=2 LOOP = (mutex.down -> enter -> exit -> mutex.up -> LOOP). ||SEMADEMO = (p[1..N]:LOOP           || {p[1..N]}::mutex:SEMAPHORE(1)).

The abstract states of interest here are when each LOOP process enters its critical section. We express these states with fluents:

 fluent CRITICAL[i:1..N] = <p[i].enter, p[i].exit>

We can express the situation in which two processes are in their critical sections at the same time as CRITICAL[1] && CRITICAL[2]. This situation must be avoided at all costs since it violates mutual exclusion. How do we assert that this situation does not occur at any point in the execution of the SEMADEMO system?

The linear temporal logic formula []F – always F – is true if and only if the formula F is true at the current instant and at all instants in the future.

Given this operator, we can now express the property that at all times in any execution of the system, CRITICAL[1] && CRITICAL[2] must not occur. This is:

 assert MUTEX = []!(CRITICAL[1] && CRITICAL[2])

This property is checked by compiling it into a safety property process. As described in Chapter 7, the check is then performed by composing this property with the system and performing an exhaustive search for the ERROR state. The property process compiled from MUTEX above is depicted in Figure 14.1.

Figure 14.1: MUTEX property process.

The MUTEX property is not violated with the semaphore initialized to one; however if we initialize the semaphore to two (i.e. SEMAPHORE(2)) then a check of the MUTEX property against the SEMADEMO system produces the following trace:

 Trace to property violation in MUTEX:       p.1.mutex.down       p.1.enter           CRITICAL.1       p.2.mutex.down      CRITICAL.1       p.2.enter           CRITICAL.1 && CRITICAL.2

The LTSA annotates the trace with the names of the fluents that are true when the action on the left occurs. So, when the action p.2.enter occurs, both of the CRITICAL fluents are true, violating mutual exclusion. The general expression of the mutual exclusion property for N processes is:

 assert MUTEX_N = []!(exists [i:1..N-1]                  (CRITICAL[i] && CRITICAL[i+1..N]))

This asserts that it is always the case that no pair of processes exist with CRITICAL true. CRITICAL[i+1..N] is a short form for the disjunction exists [j:i+1..N] CRITICAL[j].

Single-Lane Bridge Safety Property

The single-lane bridge problem was described in section 7.2. The required safety property was that it should never be the case that a red car (moving from left to right) should be on the bridge at the same time as a blue car (moving from right to left). The following fluents capture the states of red cars and blue cars being on the bridge.

 const N =3     // number of each type of car range ID= 1..N // car identities fluent RED[i:ID]  = <red[i].enter, red[i].exit> fluent BLUE[i:ID] = <blue[i].enter, blue[i].exit>

The situation in which one or more red cars are on the bridge is described by the fluent expression exists[i:ID] RED[i] and similarly for blue cars exists[j:ID] BLUE[j].The required ONEWAY property asserts that these two propositions should never hold at the same time.

 assert ONEWAY = []!(exists[i:ID] RED[i]                  && exists[j:ID] BLUE[j])

When checked in the context described in section 7.2.1 with no BRIDGE process to constrain car behavior, the following safety violation is produced:

 Trace to property violation in ONEWAY:          red.1.enter      RED.1          blue.1.enter     RED.1 && BLUE.1

Since propositions of the form exists[i:R] FL[i] can be expressed succinctly as FL[R], we can rewrite ONEWAY above as:

 assert ONEWAY = []!(RED[ID] && BLUE[ID])

This is a considerably more concise description of the required property than that achieved using property processes in section 7.2.1. In addition, it expresses the required property more directly. This is usually the case where a safety property can be expressed as a relationship between abstract states of the system described as fluents. Unsurprisingly where the required property is concerned with the permitted order of actions, direct specification using property processes is usually best.

Finally, safety properties of the form []P as we have described here are by far the commonest form of safety properties expressed in temporal logic; however, there are many other forms of safety properties which use additional temporal operators. These operators are described later.

14.2.2 Liveness Properties

A safety property asserts that nothing bad ever happens whereas a liveness property asserts that something good eventually happens. Linear temporal logic provides the eventually operator which allows us to directly express the progress properties we introduced in Chapter 7.

The linear temporal logic formula <> F – eventually F –is true if and only if the formula F is true at the current instant or at some instant in the future.

We can now assert for the single-lane bridge example that eventually the first red car must enter the bridge:

 assert FIRSTRED = <>red[1].enter

This is compiled into the transition system shown in Figure 14.2. This is a special form of transition system known as a Büchi automaton after its originator. A Büchi automaton recognizes an infinite trace if that trace passes through an acceptance state infinitely often. The example of Figure 14.2 has a single acceptance state marked by two concentric rings. It should be clear that any trace containing the action red[1].enter is not accepted by this automaton since the action will move the automaton irretrievably out of the initial acceptance state.

Figure 14.2: Büchi automaton for FIRSTRED.

In fact, the Büchi automaton of Figure 14.2 accepts the set of infinite traces represented by the negation of the FIRSTRED property – that is, !<>red[1].enter. To check whether an assertion holds, the LTSA constructs a Büchi automaton for the negation of the assertion and then checks whether there are any infinite traces that are accepted when the automaton is combined with the model. This check can be performed efficiently since it is a search for acceptance states in strongly connected components. If none are found then there is no trace that satisfies the negation of the property and consequently the property holds. We discussed strongly connected components and their relationship to infinite executions in Chapter 7. In checking liveness properties, we make exactly the same fair choice assumption as was made in Chapter 7. The property is satisfied for the basic bridge model but not for the congested model defined by:

 ||CongestedBridge       = SingleLaneBridge >> {red[ID].exit,blue[ID].exit}.

The following property violation is reported for a system with two red cars and two blue cars:

 Violation of LTL property: @FIRSTRED Trace to terminal set of states:       blue.1.enter Cycle in terminal set:       blue.2.enter       blue.1.exit       blue.1.enter       blue.2.exit LTL Property Check in: 10ms

The model, combined with the FIRSTRED property, is shown in Figure 14.3. The connected component (states 1,2,3,4) containing acceptance states can clearly be seen.

Figure 14.3: CongestedBridge showing acceptance states.

The property FIRSTRED is satisfied if the first red car enters the bridge a single time. However, the required liveness property in Chapter 7 is that red cars (and blue cars) get to enter the bridge infinitely often. In other words, it is always the case that a car eventually enters. This is exactly the condition expressed by progress properties. We can now restate those for the single lane bridge in linear temporal logic as:

 assert REDCROSS  = []<>red[ID].enter assert BLUECROSS = []<>blue[ID].enter assert CROSS = (REDCROSS && BLUECROSS)

The CROSS property is defined as the conjunction of REDCROSS and BLUECROSS and permits these properties to be checked at the same time. The Büchi automaton for the negation of REDCROSS is depicted in Figure 14.4.

Figure 14.4: REDCROSS Büchi automaton.

In a parallel composition, * synchronizes the transition it labels with all other transitions in the model, i.e. excluding actions red[1].enter and red[2].enter, but including those labeled by the silent action. It can be seen that the always part of the assertion is captured here by the non-deterministic choice on * which means that at any point in a trace, the automaton can move to state 1.

It could be argued that REDCROSS and BLUECROSS are too weak a specification of the required liveness since they are satisfied if either car 1 or car 2 crosses infinitely often. For example, the properties can be satisfied if car 2 never crosses. This is because, as mentioned previously, a set of actions is treated as a disjunction and so the property REDCROSS is:

 assert REDCROSS = []<>(red[1].enter | | red[2].enter)

A stronger assertion would be:

 assert STRONGRED = forall[i:ID] []<>red[i].enter

Response Properties

Suppose we wished to assert the liveness property that if a car enters the bridge then it should eventually exit. In other words, it does not stop in the middle or fall over the side! We can specify this property for a car as follows:

 assert REDEXIT = [](red[1].enter -> <>red[1].exit)

The corresponding Büchi automaton (for the negation) is shown in Figure 14.5.

Figure 14.5: REDEXIT Büchi automaton.

The property holds for both SingleLaneBridge and CongestedBridge. Although cars may not ever enter the congested bridge, if they do enter, they also exit. Consequently, the property is not violated. This is an extremely common form of liveness property which is sometimes termed a “response” property since it is of the form [](request -> <>reply). Note that this form of liveness property cannot be specified using the progress properties of Chapter 7.