Syntax and Semantics of Petri Nets

Petri nets are one of the most popular tools for modelling distributed systems. This book provides a modern look at the theory behind them, by studying three classes of nets that model (i) sequential systems, (ii) non-communicating parallel systems, and (iii) communicating parallel systems. A suitable behavioural equivalence is presented for each class, followed by a modal logic characterization for each equivalence. The author then introduces a suitable process algebra for the corresponding class of nets and proves that the behavioral equivalence proposed for each class is a congruence for the operator of the corresponding process algebra. Finally, an axiomatization of the behavioral congruence is proposed. The theory is introduced step-by-step, with ordinary-language explanations and examples provided throughout, to remain accessible to readers without specialized training in concurrency theory or formal logic. Exercises with solutions solidify the reader’s understanding, and the final chapter hints at possible extensions of the theory.