Free Choice Petri Nets without frozen tokens and Bipolar Synchronization Systems

TL;DR

This paper proves a new condition under which bipolar synchronization systems (BP-systems), a class of coloured Petri nets, are live and safe, extending previous theoretical results and confirming an older conjecture.

Contribution

It establishes a necessary and sufficient condition for BP-systems to be live and safe, linking properties of their underlying T-systems and free-choice nets, and confirms an elder conjecture.

Findings

BP-systems are live and safe if their T-systems and free-choice nets are live and safe.

No frozen tokens in the free-choice net ensures BP-system safety.

The result is a converse to a known theorem, completing the theoretical framework.

Abstract

Bipolar synchronization systems (BP-systems) constitute a class of coloured Petri nets, well suited for modeling the control flow of discrete, dynamical systems. Every BP-system has an underlying ordinary Petri net, which is a T-system. Moreover, it has a second ordinary net attached, which is a free-choice system. We prove that a BP-system is live and safe if the T-system and the free-choice system are live and safe and if the free-choice system has no frozen tokens. This result is the converse of a theorem of Genrich and Thiagarajan and proves an elder conjecture. The proof compares the different Petri nets by Petri net morphisms and makes use of the classical theory of free-choice systems