可达判定Petri网模型

多项式时间判定

通过结构修饰将状态方程的非负整数解数量限制为一个，在保持系统功能的同时将可达性判定问题从不可判定转化为多项式时间可判定，为 Petri 网的工业应用扫清障碍。

Su, Yue · Zhou, Mengchu · 亓亮 · Wisniewski, Remigiusz

IEEE Transactions on Systems, Man, and Cybernetics: Systems 2024

参数信息

状态方程非负整数解数量

1

技术优势

可达性可判定

将状态方程的非负整数解数量限制为不超过一个，可达性判定从不可判定转化为多项式时间可判定。

保持系统功能

结构修饰不改变被建模系统的功能，使得建模分析更加实用。

算法高效

算法在案例和实验中验证了正确性和时间效率，为工业应用提供保障。

应用场景

• 离散事件系统建模：利用可达性可判定的 Petri 网模型进行离散事件系统建模与验证。
• 机器人任务规划：用可达性可判定的 Petri 网为机器人任务规划建立可验证的模型。
• 制造系统分析：对制造系统进行可达性可判定的建模与分析，提高工业适用性。
• 多智能体协调：为多智能体协调系统提供可达性可判定的 Petri 网建模方法。
• 智能体行为验证：利用多项式时间可达性判定验证智能体行为属性。