Tutorial LTL Counter-example View

In this tutorial a quick overview will be given describing the LTL counter-example visualization plug-in in Rodin. The functionality of the plug-in will be presented by means of an Event-B model on which different properties will be checked that are not satisfied by the model.

LTL Model Checking and the Meaning of Counter-examples

Model checking is a technique for checking in an automatic way whether a model satisfies a property expressed in formal logic. LTL (standing for linear temporal logic) is a version of the temporal logic used mainly for encoding time-dependent properties of systems.

Verifying whether a system fulfills an LTL property by means of model checking is realized by searching a path in the state space of the system that violates the property being checked. That is, if the system behaves in a way violating the LTL property being checked, then the erroneous behavior will be reported by returning a path (mostly infinite) representing the false behavior. Otherwise, if no counter-example was found, it will be considered that the system satisfies the LTL property.

The LTL model checker of ProB provides three types of counter-examples:

1. Finite path leading to a deadlock state (see Figure 1):
   
   
   
   
   
2. Infinite path (see Figure 2), the infinite path in this case is represented by means of a loop:
   
   
   
   
   
3. Finite path (see Figure 3). (In this case an infinite path representing the respective counter-example has been shortened in order to attract the attention to the relevant part of the counter-example).
   
   
   
   
   

The first two types of counter-examples (Figure 1 and Figure 2) constitute a violation of a liveness^[1] property, whereas the path in Figure 3 represents usually a counter-example for a safety property.

Visualization of Counter-examples in Rodin

Each state of a path in the LTL counter-example view is marked by a respective color that denotes the evaluation of an LTL formula at that state. There are three possible statuses (colors) that a state s may have in respect to an LTL formula f:

• Green: the value of f is true at s
• Red: the value of f is false at s
• Grey: the value of f cannot be determined at s (unknown value)

A state will be colored in grey if the value of the respective LTL formula cannot be determined. This may happen in case the counter-example is represented by finite path. For example, evaluating the LTL formula ‘X {p2=crit2}’ on a path of length two where the value of p2 is not equal to crit2 in both states (see Figure 4) yields the following coloring of the states in Rodin: ^[2]

Since the value of the atom ‘{p2=crit2}’ in ${\displaystyle s_{1}}$ is equal to false the value of the LTL formula ‘X {p2=crit2}’ in ${\displaystyle s_{0}}$ is also equal to false. Therefore the first state is colored in red. On the other hand, the value of the formula ‘X {p2=crit2}’ in ${\displaystyle s_{1}}$ is unknown as there is no successor state of ${\displaystyle s_{1}}$ in the path showed in Figure 4. Accordingly, the second state in the LTL counter-example viewer will be colored in grey.

States in the path considered to be significant for the evaluation of the respective LTL formula are highlighted by bright colors. Accordingly, the other states will be grayed out.

Consider the path in Figure 5 that can be reported as a counter-example for the LTL formula ‘{p1=noncrit1} U {p1=crit1}’. ^[3] As a result the LTL counter-example view will display the following visualization of the counter-example:

The path in Figure 5 violates ‘{p1=noncrit1} U {p1=crit1}’ since the goal (‘{p1=crit1}’) of the until-formula does not hold in all states of the path. This is illustrated by means of the bottom colored path in the picture above. Both states have been colored with bright red as both are significant for the violation of the until-formula in regard to ‘{p1=crit1}’.

The upper path in the picture above has been evaluated and colored in regard to the condition (‘{p1=noncrit1}’) of the until-formula. The critical state here is the second one as ‘{p1=noncrit1}’ does not hold in that state and therefore is it highlighted by a brighter color. On the other hand, the atom ‘{p1=noncrit1}’ holds in ${\displaystyle s_{0}}$ and thus the state is colored in green. ${\displaystyle s_{0}}$ has been grayed out since the evaluation of ‘{p1=noncrit1}’ in that state has no significant meaning for the violation of ‘{p1=noncrit1} U {p1=crit1}’.

Notice, for a given LTL formula f the values (or the colors) of the states are set in regard to the evaluation of the sub-formula/-s of f and highlighted with respect to the semantics of f. In case of the formula ‘{p1=noncrit1} U {p1=crit1}’ the states are colored in regard to the atoms ‘{p1=noncrit1}’ and ‘{p1=crit1}’ and highlighted in regard to the semantics of the until-operator.

A path reported as a counter-example of an LTL formula represents a possible trace of the model being analyzed. In some cases it may be helpful to know which transitions are executed along the path in order to reproduce the erroneous behavior of the model (e.g. by animating the trace). To see which transitions are being executed in the counter-example hold the mouse cursor on the respective edge. A label will come up with the transition name:

Another way to find out the transitions of the path is to inspect the current trace loaded in the history view.

To view a state of a counter-example showed in the LTL counter-example view perform a double-click action on the respective state. After double-clicking a state the relevant information (variables’ evaluation, invariant evaluation, etc.) of the state is displayed in the state view and the trace leading to the double-clicked state is loaded in the history view.

The counter-example reported by the LTL model checker will be visualized in regard to all operators used in the LTL formula. For example, three different visualizations will be illustrated for ‘G ({p1=wait1} => F {p1=crit1})’ as shown in the picture below. ^[4]:

In order to view the visualizations of the sub-formulas, one should click on one of the states of the source-formula.

Use Case for the LTL Counter-example Viewer

Consider an Event-B model formalizing an algorithm for mutual exclusion with semaphores for two concurrent processes ${\displaystyle P_{1}}$ and ${\displaystyle P_{2}}$. Each process has been simplified to perform three types of events: request (for entering in the critical section), enter (entering the critical section), and release (exiting the critical section).

Each process ${\displaystyle P_{i}}$ has three possible states that are denoted by the constants ${\displaystyle noncrit_{i}}$ (the state in which ${\displaystyle P_{i}}$performs noncritical actions), ${\displaystyle wait_{i}}$ (the state in which ${\displaystyle P_{i}}$ waits to enter the critical section), and ${\displaystyle crit_{i}}$ (representing the state in which ${\displaystyle P_{i}}$ is in the critical section). Both processes share the binary semaphore y where y=1 indicates that the semaphore is free and y=0 that the semaphore is currently processed by one of the processes.

There are several requirements that the mutual exclusion algorithm should satisfy. The most important one is the mutual exclusion property that says always at most one process is in its critical section. This can be simply expressed, for example, as an invariant of the respective Event-B model: ‘not(p1 = crit1 & p2 = crit2)’. However, there are other properties that can be easily expressed by means of LTL formulas and automatically checked on the model. For example, the requirement each process will enter infinitely often its critical section can be specified by the LTL formula `GF {p1 = crit1} & GF {p2 = crit2}` and the starvation freedom property that states each waiting process will eventually enter its critical section can be encoded in LTL by means of the formula `G ({p1 = wait1} => F {p1 = crit1}) & G ({p2 = wait2} => F {p2=crit2}) `.

The second requirement each process will enter infinitely often its critical section can be divided in two single requirements:

1. Process 1 will enter infinitely often its critical section (‘GF {p1=crit1}’)
2. Process 2 will enter infinitely often its critical section (‘GF {p2=crit2}’)

Running the LTL model checker of ProB with the LTL formula ‘GF {p1=crit1}’ on the MUTEX model will provide the following path as a counter-example, where the equations in the set braces represent the current variables’ evaluation in the respective state and the labels above the edges the executed events in the path:

Obviously the property ‘GF {p1=crit1}’ is violated for the path in Figure 6 since it constitutes an infinite path where no state exists in which p1 is equal to crit1. The counter-example for ‘GF {p1=crit1}’ will be then visualized as follows:

Each state of the counter-example is colored in red since ‘F {p1=crit1}’ does not hold in all states of the path. Additionally, state ${\displaystyle s_{0}}$ has been highlighted since all paths starting at ${\displaystyle s_{0}}$ do not satisfy ‘F {p1=crit1}’.

To see why the LTL formula ‘F {p1=crit1}’ does not hold in each state of the path in Figure 6 click on one of the nodes in the visualization. As a consequence a second box will appear visualizing the counter-example in regard to the LTL formula ‘F {p1=crit1}’. In the second visualization all states are colored in red since ‘{p1=crit1}’ does not hold in all states. All states are highlighted as well since ‘F {p1=crit1}’ holds if and only if there is a state in which p1 is equal to crit1 and thus all states are significant for the violation of the formula.

For the starvation freedom property (each waiting process will eventually enter its critical section) of process P1 three operators are needed for encoding it in LTL: ‘G ({p1=wait1} => F {p1=crit1})’. The mutual exclusion model violates the property because it permits the second process P2 to perform infinitely often consecutively the events Req2, Enter2, Rel2 and thus not allowing process P1 to get access to its critical section. This means that the path in Figure 6 may also be reported as a counter-example for: ‘G ({p1=wait1} => F {p1=crit1})’ by the LTL model checker. As a consequence, the following visualization will be shown in the LTL counter-example view:

In this visualization the crucial state for violating the property ‘G ({p1=wait1} => F {p1=crit1})’ is ${\displaystyle s_{1}}$ since at this state ‘{p1=wait1}’ becomes true. Once a state is encountered where ‘{p1=wait1}’ holds, it should be guaranteed that eventually ‘{p1=crit1}’ will hold. This is apparently not fulfilled as in all successor states p1 will not become equal to crit1.

Literature Sources

For more detailed information on visualizing counter-examples in the LTL counter-example view in Rodin refer to ^[5]. For a thorough introduction to LTL and LTL model checking consult ^[6] or ^[7].

The Event-B model used in this tutorial can be downloaded from here.

References and Notes