Petri网可达性分析的代数方法

摘要

可达性是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网的可达性进行判定。

目录

封面

声明

中文摘要

英文摘要

目录

Contents

1 引 言

1.1 选题背景

1.2 研究现状

1.3 研究方法

1.4 内容组织

2 Petri网基础

2.1 网与网系统

2.2 Petri网的动态性质

2.3 Petri网的分析方法

2.4 Petri网的结构性质

3 S-不变量的求取及其在可达性判定中的应用

3.1 S-不变量基本概念

3.2 S-不变量极小支集的判定

3.3 S-不变量的求取

3.4 S-不变量与不可达性判定

4 加模S-不变量与不可达判定

4.1 加模S-不变量的概念及其性质

4.2 初等整数变换与整数矩阵分解

4.3 加模S-不变量的求取

4.4 基于加模S-不变量的不可达判定

5 状态方程与可达方程

5.1 状态方程解的存在性与不可达判定

5.2 不可达标识分类

5.3 可达性等价于状态方程可满足性的Petri网子类

5.4 状态方程的求解

5.5 可达方程

6 结束语

6.1 主要成果

6.2 下一步的工作

附 录

致谢

参考文献

在读期间的研究成果