algorithm - 有色 Petri 网的边界准则

Question

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

Answer 1

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