基于极小T-不变量增加的Petri网可达性分析

Petri网是一种图形化和数学化的建模工具，具有描述同步、并发、冲突等行为的能力，已经在工作流管理、软件工程、协议验证等众多领域得到了应用。 可达性是描述Petri网状态和行为的一种重要而有效的手段。对于一般Petri网的可达性问题所具有的时间复杂度至少是指数级的。为了简化可达性分析，我们提出了一种基于T-不变量增加的Petri网的可达性分析方法。 对于一类含T-不变量的Petri网，基于T-不变量增加的Petri网的可达性分析过程如下：首先，通过定义一个Petri网的b-路线性约束问题，即对网的状态方程加以适当的约束，求得一组特征解向量。b-路线性约束问题对Petri网的状态方程的解进行了约束，这一过程的作用是将状态方程的无穷解空间缩小为一个有限的解空间，并且这个有限解空间中的每一个特征解向量的分量和不超过 ( 为给定网的变迁个数)；其次，如果求得的特征解向量使得初始状态到目标状态可达，那么可达性问题就可解决，如果不能使得初始状态到目标状态可达，那么在特征解向量的基础上适当添加整数倍极小T-不变量使得这个添加后的特征解向量形式上可达。这个过程需要运用扩展极小T-不变量关系图和扩展借矩阵，并且保证添加极小T-不变量后的特征解向量的分量小于 （我们称满足这个条件的可达为b-路可达），然后再判断这个添加极小T-不变量后的特征解向量的可达性。该方法的优点在于判断的变迁向量较短，从而在一定程度上简化可达性分析的过程。