Free Choice Petri Nets without frozen tokens and Bipolar Synchronization Systems
<|reference_start|>Free Choice Petri Nets without frozen tokens and Bipolar Synchronization Systems: 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<|reference_end|>
@article{wehler2006free,
    title={Free Choice Petri Nets without frozen tokens and Bipolar Synchronization
  Systems},
    author={Joachim Wehler},
    journal={arXiv preprint arXiv:cs/0609095},
    year={2006},
    archivePrefix={arXiv},
    eprint={cs/0609095},
    primaryClass={cs.LO}
}