Other research on partial order semantics

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.

• left-handed philosophers, which always take the left fork before the right one.
• right-handed philosophers, which alwas take the right fork before th left one.
• ambidextrous philosophers, which can take both forks concurrently.

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

• in graph-theoretical terms, as the maximal cliques of a certain graph,
• in algebraic terms, as the set of integer solutions of a linear set of equations, and
• in logical terms, as the set of models of a propositional formula.

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:

• Semantics. Papers in this category give an occurrence net semantics to different models of concurrency, including Petri nets of various kinds, synchronous products of concurrent systems, and process algebras.
• Algorithmics. Papers in this category propose algorithms to construct finite complete prefixes, and to check properties on the unfolding of the system like deadlock freedom, reachability, or properties expressed using temporal logics.
• Applications. Papers in this category apply unfolding techniques to the verification of circuits, telecomunication systems, distributed algorithms, and others.
• Tools. Papers in this category describe software developments for the simulation and verification of systems using unfoldings.

• All references

Decidability of partial order equivalences

Cooperations

• University of Oldenburg (Eike Best),
• Humboldt University, Berlin (Peter Starke),
• University of Augsburg (Walter Vogler),
• University of Aizu, Japan (Alex Kondratyev, Alex Taubin),
• University of Newcastle upon Tyne, Britain (Alex Yakovlex).

Publications

[Esp94b]

J. Esparza.
Model checking using net unfoldings.
Science of Computer Programming, 23:151-195, 1994.
Abstract: McMillan (1992) described a technique for deadlock detection based on net unfoldings. We extend its applicability to the properties of a temporal logic with a possibility operator. The new algorithm is shown to be polynomial in the size of the net for 1-safe conflict free Petri nets, while the algorithms of the literature require exponential time.

[eskiehn95]

J. Esparza and A. Kiehn.
On the model checking problem for branching logic and Basic Parallel Processes.
In Proceedings of CAV '95, number 939, pages 353-366. Springer-Verlag, 1995.
Abstract: We investigate the model checking problem for branching time logics and Basic Parallel Processes. We show that the problem is undecidable for a logic equivalent to $CTL*$ in the usual interleaving semantics, but decidable in a standard partial order interpretation.

[EM97]

J. Esparza and S. Melzer.
Model checking LTL using constraint programming.
In Proc. of Application and Theory of Petri Nets'97, 1997. [gzipped Postscript ]
Abstract: The model-checking problem for 1-safe Petri nets and linear-time temporal logic (LTL) consists of deciding, given a 1-safe Petri net and a formula of LTL, whether the Petri net satisfies the property encoded by the formula. This paper introduces a semidecision test for this problem. By a semidecision test we understand a procedure which may answer `yes', in which case the Petri net satisfies the property, or `don't know'. The test is based on a variant of the so called automata-theoretic approach to model-checking and on the notion of T-invariant. We analyse the computational complexity of the test, implement it using 2lp - a constraint programming tool, and apply it to two case studies.

[EM99]

J. Esparza and S. Melzer.
Verification of safety properties using integer programming: Beyond the state equation.
Formal Methods in System Design, 1999.
to appear. [gzipped Postscript ]
Abstract: The state equation is a verification technique that has been applied - not always under this name - to numerous systems modelled as Petri nets or communicating automata. Given a safety property P, the state equation is used to derive a necessary condition for P to hold which can be mechanically checked. The necessary conditions derived from the state equation are known to be of little use for systems communicating by means of shared variables, in the sense that many of these systems satisfying the property but not the conditions. In this paper, we use traps, a well-known notion of net theory, to obtain stronger conditions that can still be efficiently checked. We show that the new conditions significantly extend the range of verifiable systems.

[ERV96]

J. Esparza, S. Römer, and W. Vogler.
An improvement of MacMillan's unfolding algorithm.
In T. Margaria and B. Steffen, editors, Proc. of TACAS'96, number 1055, pages 87-106. Springer-Verlag, 1996. [gzipped Postscript ]
Abstract: McMillan has proposed a new technique to avoid the state explosion problem in the verification of systems modelled with finite-state Petri nets. The technique is based on the concept of net unfolding, a well known partial order semantics of Petri nets, later described in more detail under the name of 'branching processes'. The unfolding of a net is another net, usually infinite but with a simpler structure. McMillan proposes an algorithm for the construction of a finite initial part of the unfolding which contains full information about the reachable states. We call such an initial part a finite complete prefix. He then shows how to use these prefixes for deadlock detection. Although McMillan's algorithm is simple and elegant, it sometimes generates prefixes much larger than necessary. In some cases a minimal complete prefix has O(n) in the size of the Petri net, while the algorithm generates a prefix of size $O(2n)$. In this paper we provide an algorithm which generates a minimal complete prefix (in a certain sense to be defined). The prefix is always smallerthan or as large as the prefix generated with the old algorithm.

[HNW98]

M. Huhn, P. Niebert, and F. Wallner.
Verification based on local states.
In Proc. of TACAS'98, number 1384, pages 35-51. Springer-Verlag, 1998. [gzipped Postscript ]
Abstract: Net unfoldings are a well-known partial order semantics for Petri nets. Here we show that they are well suited to act as models for branching-time logics interpreted on local states. Such local logics (in particular a "distributed mu-calculus") can be used to express properties from the point of view of one component in a distributed system. Local logics often allow for more efficient verification procedures because - in contrast to interleaving branching-time logics - they do not refer to the entire space of global states. We reduce verification of local properties to standard model checking algorithms known for interleaving branching-time logics. The key is to extract a finite (usually small), local transition system bisimilar to the complete unfolding. The construction is based on the finite prefix of a net unfolding defined by McMillan.

[HNW99]

M. Huhn, P. Niebert, and F. Wallner.
Model checking logics for communicating sequential agents.
In Proc. of FOSSACS'99, number 1578, pages 227-242. Springer-Verlag, 1999. [gzipped Postscript ]
Abstract: We present a model checking technique for $L$_csa , a temporal logic for communicating sequential agents (CSAs) introduced by Lodaya, Ramanujam, and Thiagarajan. $L$_csa contains temporal modalities indexed with a local point of view of one agent and allows to refer to properties of other agents according to the latest gossip which is related to local knowledge. The model checking procedure relies on a modularisation of $L$_csa into temporal and gossip modalities. We introduce a hierarchy of formulae and a corresponding hierarchy of equivalences, which allows to compute for each formula and finite state distributed system a finite multi modal Kripke structure, on which the formula can be checked with standard techniques.

[KH97]

A. Kiehn and M. Hennessy.
On the decidability of non-interleaving process equivalences.
Fundamenta Informaticae, 30:23-43, 1997.
Abstract: We develop decision procedures based on proof tableaux for a number of non-interleaving equivalences over processes. The processes considered are those which can be described in a simple extension of $BPP$_τ , Basic Parallel Processes with communication, obtained by omitting the restriction operator from $CCS$. Decision procedures are given for both strong and weak versions of location equivalence and ST-bisimulation.

[Mad97]

A. Mader.
Verification of Modal Properties Using Boolean Equation Systems.
PhD thesis, TU München, 1997.
Abstract: This thesis is concerned with model-checking in the modal $\mu$-calculus. By showing the equivalence of solving Boolean equation systems and model-checking we are also able to derive equivalences with problems in automata-theoretic and game-theoretic frameworks, which sched new light on complexity issues for model-checking. A new algorithm for solving Boolean equation systems is presented, similar to Gauß elimination for linear equation systems. For the case of systems with infinite state spaces we also prove the equivalence of model-checking and solving infinite Boolean equation systems, and derive an algorithm for it.

[ME96]

S. Melzer and J. Esparza.
Checking system properties via integer programming.
In Proc. of ESOP'96. Springer-Verlag, 1996. [gzipped Postscript ]
Abstract: The marking equation is a well known verification method in the Petri net community. It has also be applied by Avrunin, Corbett et al. to automata models. It is a semidecision method, and it may fail to give an answer for some systems, in particular for those communicating by means of shared variables. In this paper, we complement the marking equation by a so called trap equation. We show that both together significantly extend the range of verifiable systems by conducting several case studies.

[MR97]

S. Melzer and S. Römer.
Deadlock checking using net unfoldings.
In Proc. of the Conf. on Computer-Aided Verfication (CAV'97), 1997. [gzipped Postscript ]
Abstract: McMillan presented a deadlock detection technique based on unfoldings of Petri n et systems. It is realized by means of a backtracking algorithm that has its drawback for unfoldings that increase widely. We present an approach that exploits precisely this property. Moreover, we introduce a fast implementation of McMillan's algorithm and compare it with our new technique.

[Mer97]

S. Merkel.
Verification of fault tolerant algorithms using pep.
SFB-Report TUM-I9734 342/23/97A, TU München, Dept. of Computer Science, 1997.
Abstract: Petri net theory is an accepted approach to modelling and verifying distributed algorithms. In this paper we show how a tool based on Petri net theory, the PEP tool, can be used to model and verify fault tolerant algorithms for distributed systems. We conduct three case studies to illustrate our approach and to show the more specific problems we ran into, such as synchronization and crash detection in asynchronous systems, and we explain how we tried to solve them.

[Roe95]

C. Röckl.
Proof tableaux for basic parallel processes.
Technical report, TU München, Dept. of Computer Science, 1995.
Term project.
Abstract: Due to their constructiveness, recent proofs of the decidability of the strong bisimulation equivalence and the local cause equivalence of recursive BPP (Basic Parallel Processes) have provided algorithms based on the underlying tableau systems. The work in hand compares two just slightly distinct proof systems, the first of them testing on the strong bisimulation equivalence of BPP and the second testing on a more restricted notion of equivalence, the local cause equivalence. The latter is not merely a subclass of the former, but a proper one, for which a standard example will be given. Annotated to this work is a Scheme program executing both the proof utilising strong bisimulation and the one utilising local cause bisimulation upon BPP.

[Wal98]

F. Wallner.
Model checking LTL using net unfoldings.
In Prof. of CAV'98, number 1427, pages 207-218. Springer-Verlag, 1998. [gzipped Postscript ]
Abstract: Net unfoldings are a well-studied partial order semantics for Petri nets. In this paper, we show that the finite prefix of an unfolding, introduced by McMillan, is suited for model checking linear-time temporal properties. The method is based on the so-called automata-theoretic approach to model checking. We propose a technique to treat this approach within the framework of safe Petri nets, and give an efficient algorithm for detecting the system runs violating a given specification.

[Wim97]

G. Wimmel.
A bdd based model checker for the pep tool.
Technical report, TU München, Dept. of Computer Science, 1997.
Term project. [gzipped Postscript ]
Abstract: PEP (Programming Environment based on Petri Nets) is a tool developed at the University of Hildesheim. It can be used for editing, simulating and verifying Petri nets, and for creating Petri nets from a program in an imperative programming language. For the verification task, model checkers are used to decide whether a given logical formula is true or false for a particular Petri net. A fairly new method in implementing model checkers, symbolic model checking, involves binary decision diagrams (BDDs), a data structure for representing considerably large state spaces. In the individual project described in this dissertation, a BDD-based model checker for the PEP tool was developed that can verify safe Petri nets. The model checker makes use of the SMV system, developed at the Carnegie Mellon University. In addition, a range of different modelling possibilities, model checking options and optimisation techniques is discussed and evaluated using examples like the dining philosophers problem. The performance of BDD-based Petri net model checking is compared to the performance of the partial order model checker that is already implemented in the PEP Tool.

Tools

• An efficient implementation of the algorithm to construct a complete prefix.
• A deadlock checker.
• A reachability checker.
• An LTL model checker.

• Mole - A Petri Net unfolder

Links to Related Sites

• World of Petri Nets: Homepage of the International Petri Net Community