论文部分内容阅读
可达性是Petri网最基本最重要的一种动态性质，其判定问题是Petri网理论研究的重要课题。本文借助代数方法对可达性进行分析，研究内容包括以下方面：(1)提出标识的不可达见证向量的概念，并给出两类不可达见证向量的求取方法。第一类见证向量来自于网的S-不变量。为求取此类见证向量，文中将给出几种求取S-不变量的新算法。其中，STRK算法能在多项式时间复杂度内求得部分极小支集上的极小S-不变量；SRK算法对任意网都能求出至少一个立于极小支集上的极小S-不变量(只要该网存在S-不变量)，而且，SRK算法平均情况下具有多项式时间复杂度；此外，ERK算法能求出全部极小支集上的极小S-不变量，EERK算法能求出全部极小S-不变量。第二类见证向量来自于网的加模S-不变量。文中首先给出初等整数变换的概念，之后借助初等整数变换对整数矩阵进行分解，并在此基础上给出从加模S-不变量中求取不可达见证向量的方法。(2)给出状态方程实数解、有理数解、整数解及非负整数解存在性的判定方法，分析状态方程各类解的存在性与S-不变量、加模S-不变量以及死锁和陷阱在不可达判定中的关系，对不可达标识进行分类。此外，给出一个求取状态方程非负整数解的新算法。(3)提出极小陷阱回路网、变迁单输入回路网、极小变迁单输入陷阱回路网以及极小死锁回路网、变迁单输出回路网和极小变迁单输出死锁回路网的概念。对于初始标识下不含空极小回路的陷阱回路网、极小陷阱回路网、变迁单输入回路网和极小变迁单输入陷阱回路网，以及目标标识下不含空极小回路的死锁回路网、极小死锁回路网、变迁单输出回路网以及极小变迁单输出死锁回路网，证明这些Petri网子类的可达性等价于状态方程的可满足性。(4)对可达性与可达方程可满足性相互等价的证明进行补充，给出一个判定非负整数向量是否为可执行向量的判定算法，最后利用该算法对唯一可达向量网和不含T-不变量的Petri网的可达性进行判定。