Compositional model checking of concurrent systems, with Petri nets

Paweł Sobociński
(University of Southampton)

Compositionality and process equivalence are both standard concepts of process algebra. Compositionality means that the behaviour of a compound system relies only on the behaviour of its components, i.e. there is no emergent behaviour. Process equivalence means that the explicit statespace of a system takes a back seat to its interaction patterns: the information that an environment can obtain though interaction.

Petri nets are a classical, yet widely used and understood, model of concurrency. Nevertheless, they have often been described as a non-compositional model, and tools tend to deal with monolithic, globally-specified models.

This tutorial paper concentrates on Petri Nets with Boundaries (PNB): a compositional, graphical algebra of 1-safe nets, and its applications to reachability checking within the tool Penrose. The algorithms feature the use of compositionality and process equivalence, a powerful combination that can be harnessed to improve the performance of checking reachability and coverability in several common examples where Petri nets model realistic concurrent systems.

Invited Presentation in César A. Muñoz and Jorge A. Pérez: Proceedings of the Eleventh International Workshop on Developments in Computational Models (DCM 2015), Cali, Colombia, October 28, 2015, Electronic Proceedings in Theoretical Computer Science 204, pp. 19–30.
Published: 2nd March 2016.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: