Since 1994 we are working on the development of a model-checking technique for the verification of concurrent systems. The technique is based on the concept of net unfoldings, a well-known partial order semantics originally introduced for Petri nets by Nielsen, Plotkin and Winskel in 1980 [NPW80]. It can be applied to different models of concurrency, like Petri nets, different classes of communicating automata, and simple process algebras.
The unfolding of a system is an occurrence net, a particularly simple Petri net without cycles. A concurrent system (think of it as a tuple of communicating transition systems) is to its unfolding what a single transition system is to its unwinding into a tree.
The unfolding of a concurrent system is behaviourally equivalent to it, in the same way that the unwinding of a transition system is behaviourally equivalent to the transition system itself. To make this statement precise you can choose your favourite notion of equivalence: Trace-, failures-, bisimulation-equivalence, or even so called true concurrency equivalences, like history-preserving bisimulation ..., which not only preserve the possible execution sequences and the branching structure, but also the concurrency of the system.
Unfoldings are usually infinite nets, and so they cannot be directly stored in a computer. However, K. McMillan observed in his Ph. D. Thesis [McM93] that it is possible to construct a finite initial part of the unfolding containing as much information as the unfolding itself. We call such an initial part a finite complete prefix. The set of reachable states of a finite complete prefix coincides with the set of reachable states of the system. Finite complete prefixes can be generated, stored in a computer, and use to check behavioural properties.
One of the advantages of complete prefixes is that they can be much smaller than the state space of the system, and (if adequate algorithms are used) never larger (see How big are complete prefixes? ). Therefore, they are a useful technique to attack the well-known state explosion problem. The price to pay is that extracting information from a prefix (for instance, whether the system is deadlock-free) is more expensive than extracting it from a transition system (see How are properties checked with complete prefixes?); Fortunately, in many examples this price turns out to be very affordable.
The second advantage of unfoldings is that they contain information about causality, spatial distribution, and concurrency. Using this information it is possible to verify properties expressed in local logics, which allow to reason about the knowledge each component has of the global state of the system. A typical property of this kind is
The unfolding technique has been applied to the verification of circuits, telecomunication systems, distributed algorithms, manufacturing systems, and others.
For a list of our own publications on the unfolding technique, click
here. For a relatively complete
bibliography, click here.
Consider the system of the figure below, modelled as a Petri net.
Alternatively, we can think of this system as two communicating automata.
The states of the first automaton are s1, s3, s4, s6,
and the states of the second are s2, s5, s7. The automata
synchronize on the transitions t4 and t5.
How big are complete prefixes?
A complete prefix is usually much smaller than the state space of
the system. For instance, Dijkstra's dining philosophers
or Milner's scheduler have complete
prefixes that grow linearly with the number of components,
while the corresponding transition systems grow exponentially.
Complete prefixes can also be smaller than a BDD representation of
the state space, as proved
by the following little experiment. Three classes
of philosophers were considered:
4 178 94 355 52 0.30
6 583 248 1716 305 0.52
8 1553 390 8678 1437 0.92
10 3140 510 27516 4637 1.48
12 4855 632 47039 8538 1.76
14 33742 797 429903 85798 2.54
There are other systems for which the BDD representation is smaller than the complete prefix. As a rule of thumb, it can be said that BDDs exploit the regularity of a system, while unfoldings exploit its concurrency. Systems composed of tightly coupled identical components are very regular and not very concurrent, and so BDDs may have the edge. For highly concurrent systems of heterogeneous components unfoldings may be more suitable. But be prepared for many exceptions.
To close this point, it should be mentioned that current algorithms for the construction of complete finite prefixes guarantee that the prefix will never be larger than the state space. So with unfoldings one will never be worse-off in memory terms than by explicitely constructing the state space.
Ocurrence nets have a very nice property: The set of reachable states can be characterized
These characterisations allow to apply graph theoretical algorithms, tools for integer linear problems, and SAT solvers or logic programming tools to check safety properties like deadlock freedom or reachability of states. This is one of the strong points of the unfolding technique: it makes possible to apply technology developed along many years by the mathematical and logic programming communities.
In automatic verification there is a trade-off between time and space. If the system is represented in a very compact way, then extracting information from it is computationally expensive. For instance, if a concurrent system is very compactly represented as a tuple of communicating automata, or as a Petri net, then typical verification problems, like deadlock-freedom or reachability of a state, are PSPACE-complete. If we take the transition system as representation instead, then the problems are polynomial, but the size of the representation blows-up in most cases. Complete prefixes offer a compromise: their size is between the sizes of the concurrent system and the transition system, and typical problems are NP-complete. As was mentioned above, the problems can be very easily translated to standard NP-complete problems, like satisfiability of boolean formulas, or integer linear programming, in order to apply existing tools for these problems. Many instances of the problems are solved very efficiently. For the example of the random philosophers and a property like deadlock-freedom, unfoldings are much more efficient than an exhaustive exploration of the state space, and also more efficient than BDDs (at least using the BDD-package we used, and in the same way as we used it). Notice that for 14 philosophers one never has to generate a prefix containing more than 185 nodes, while one may have to generate BDDs containing over 400.000 nodes. This difference in size easily compensates for the potentially more time-consuming checking algorithms of the unfolding technique.
We try to keep a relatively complete bibliography on net unfoldings. After the last update it contains over 60 references, which can be classified into the following categories: