This paper shows how two of the most important analysis methods for Petri nets can be performed in a modular way. We illustrate our techniques by means of modular Place/Transitions nets (modular PT-nets) in which the individual modules interact via shared places and shared transitions. For place invariants we show that it is possible to construct invariants of the total modular PT-net from invariants of the individual modules. For state spaces, we show that it is possible to decide behavioural properties of the modular PT-net from state spaces of the individual modules plus a synchronization graph, without unfolding to the ordinary state space. The generalization of our techniques to high-level Petri nets is rather straightforward.

The theory behind the notions of place invariants and place flows for coloured Petri nets has been known since 1980, but the lack of tool support entails that the practical use of these results has been very limited. The aim of this paper is to help bridging the gaps between the theory and tool support related to place flows, and in this way support the practical use of place flows. There are three related problem areas to attack: finding place flows from the structure and inscriptions of CP-nets, showing how the place flows determine place invariants, and finally finding properties of CP-nets from the place invariants. We show how checking that a set of weights determines a place flow can be formulated as a /spl lambda/-expressions rewriting problem, allowing us to use the whole set of techniques developed inside the field of /spl lambda/-calculus. We also show how these techniques can be used to prove properties such as deadlock-freeness.

CCS is a universal formalism: any computable function is computed by some CCS agent. Moreover, one can reduce the halting problem for Turing machines to the problem of deciding bisimilarity of two CCS agents, thus demonstrating the undecidability of the equivalence checking problem. In this paper, we demonstrate the limits of decidability of CCS. In particular, we show that by simply disallowing either of communication or both restriction and relabelling, we arrive at a sublanguage which still describes a rich class of infinite state systems but for which bisimulation is decidable. We also demonstrate complete axiomatisations for these sublanguages. We compare these results with the undecidability of all other common equivalences.

The authors prove the decidability of two subclasses of recursive processes involving a parallel composition operator with respect to bisimulation equivalence, namely, the so-called normed and live processes. To accomplish this, the authors first prove a unique decomposition result for (a generalization of) normed processes, in order to deduce a necessary cancellation law. The decidability proof leads to a complete axiomatization for these process classes.>