Cooperations,
Financial Support
Publications, Tools Current Members: Former Members:

Since 1994 we are working on the development of a modelchecking technique for the verification of concurrent systems. The technique is based on the concept of net unfoldings, a wellknown 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, bisimulationequivalence, or even so called true concurrency equivalences, like historypreserving 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 wellknown state explosion problem. The price to pay is that extracting information from a prefix (for instance, whether the system is deadlockfree) 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.
Phil.  Aver.  Min.  Max.  St.Dev.  Aver./St.Dev 

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 
Phil.  Aver.  Min.  Max.  St.Dev.  Aver./St.Dev 

4  46  40  60  5.1  0.10 
6  70  60  85  6.0  0.09 
8  95  80  110  6.9  0.07 
10  117  100  135  7.8  0.07 
12  141  120  160  7.4  0.05 
14  161  140  185  9.3  0.06 
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 worseoff 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 tradeoff 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 deadlockfreedom or reachability of a state, are PSPACEcomplete. If we take the transition system as representation instead, then the problems are polynomial, but the size of the representation blowsup 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 NPcomplete. As was mentioned above, the problems can be very easily translated to standard NPcomplete 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 deadlockfreedom, unfoldings are much more efficient than an exhaustive exploration of the state space, and also more efficient than BDDs (at least using the BDDpackage 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 timeconsuming 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: