无冻结记号的自由选择 Petri 网与双极同步系统
计算机科学中的逻辑
2007-09-10 v2
摘要
双极同步系统 (BP 系统) 是一类彩色 Petri 网，适合建模离散动态系统的控制流。每个 BP 系统都有一个底层的普通 Petri 网，即 T 系统。此外，它还附加有一个自由选择系统。我们证明了如果 T 系统和自由选择系统均为 live 和 safe，并且自由选择系统没有冻结记号，则 BP 系统是 live 和 safe 的。这一结果是 Genrich 和 Thiagarajan 定理的逆命题，证明了一个年长的猜想。该证明通过 Petri 网同构比较不同的 Petri 网，并运用经典的自由选择系统理论。
引用
@article{arxiv.cs/0609095,
title = {Free Choice Petri Nets without frozen tokens and Bipolar Synchronization Systems},
author = {Joachim Wehler},
journal= {arXiv preprint arXiv:cs/0609095},
year = {2007}
}