2006/09/17 by Joachim Wehler, Wehler, Joachim · 1 citation
Computer Science · #D.2.2 #Distributed systems and fault tolerance #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Petri Nets in System Modeling #cs.LO
paper · pdf · doi:10.48550/arxiv.cs/0609095
openalex publication_date 2006/09/17 · arxiv created 2007/09/10 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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