| 题名 | 基于极小T-不变量增加的Petri网可达性分析 |
| 作者 | 彭建兵 |
| 学位类别 | 硕士 |
| 答辩日期 | 2010-06-03 |
| 授予单位 | 中国科学院研究生院 |
| 授予地点 | 北京 |
| 导师 | 焦莉 |
| 关键词 | Petri网，可达性， 极小T-不变量， T-不变量关系图，借矩阵 |
| 学位专业 | 计算机软件与理论 |
| 中文摘要 | Petri网是一种图形化和数学化的建模工具，具有描述同步、并发、冲突等行为的能力，已经在工作流管理、软件工程、协议验证等众多领域得到了应用。 可达性是描述Petri网状态和行为的一种重要而有效的手段。对于一般Petri网的可达性问题所具有的时间复杂度至少是指数级的。为了简化可达性分析，我们提出了一种基于T-不变量增加的Petri网的可达性分析方法。 对于一类含T-不变量的Petri网，基于T-不变量增加的Petri网的可达性分析过程如下：首先，通过定义一个Petri网的b-路线性约束问题，即对网的状态方程加以适当的约束，求得一组特征解向量。b-路线性约束问题对Petri网的状态方程的解进行了约束，这一过程的作用是将状态方程的无穷解空间缩小为一个有限的解空间，并且这个有限解空间中的每一个特征解向量的分量和不超过 ( 为给定网的变迁个数)；其次，如果求得的特征解向量使得初始状态到目标状态可达，那么可达性问题就可解决，如果不能使得初始状态到目标状态可达，那么在特征解向量的基础上适当添加整数倍极小T-不变量使得这个添加后的特征解向量形式上可达。这个过程需要运用扩展极小T-不变量关系图和扩展借矩阵，并且保证添加极小T-不变量后的特征解向量的分量小于 （我们称满足这个条件的可达为b-路可达），然后再判断这个添加极小T-不变量后的特征解向量的可达性。该方法的优点在于判断的变迁向量较短，从而在一定程度上简化可达性分析的过程。 |
| 英文摘要 | Petri nets are a graphical and mathematic modeling tool applicable to many systems. They are used for describing systems that are characterized as being concurrent, parallel, asynchronous, and have widespread applications, such as work-flow management, software engineering, protocol verification, etc. Reachability analysis of Petri nets is very important and efficient to describe the behaviors of the system, and its time complexity for general Petri nets is at least exponential time. To solve the reachability analysis, we propose a method based on minimal T-invariants adding. Reachability analysis of Petri nets based on minimal T-invariants adding includes two steps. First, we define a b-route linear constrained problem, which gives some constraint conditions to the fundamental equation of the net, then we get some characteristic vectors to solve the linear constrained problem. The step reduces the infinite solution space of the fundamental equation to a finite one, in which each solution has the sum length of the components less than nb(n is the number of transitions in the Petri net). Second, if the characteristic vector makes the target state belong to the reachability set of the net, then reachability problem is resolved; otherwise, we need to add some properly minimal T-invariants to characteristic vector by using an extended relation graph of minimal T-invariants and an extended borrowing matrix, then we determine whether or not the consequent vector can be transformed to a target state. The advantage of this step is that the length of the consequent vector is very short, which makes the determination very simple. |
| 语种 | 中文 |
| 公开日期 | 2010-06-06 |
| 内容类型 | 学位论文 |
| 源URL | [http://124.16.136.157/handle/311060/2310]  |
| 专题 | 软件研究所_计算机科学国家重点实验室 _学位论文 |
| 推荐引用方式 GB/T 7714 | 彭建兵. 基于极小T-不变量增加的Petri网可达性分析[D]. 北京. 中国科学院研究生院. 2010. |
| 个性服务 |
| 查看访问统计 |
| 相关权益政策 |
| 暂无数据 |
| 收藏/分享 |
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。
修改评论