有色 Petri 网的边界准则

Question

是否有一种算法可以检查彩色 petri 网的边界标准（意味着状态空间是有限的）（或者该属性是否不可判定）？

Answer 1

是的，如果状态空间是无限的，状态图的构造算法就会中止。 基本上，它所做的是检查它达到的每个状态，如果有另一个状态具有严格更小的标记（在至少一个组件中更小，并且在所有组件中更小或相等）可以达到当前标记。如果是这样，由于 petri 网的单调性，网络具有无限的状态空间。