位置:成果数据库 > 期刊 > 期刊详情页
一种基于进程验证的Petri网可达性判定方法
  • 期刊名称:计算机学报
  • 时间:0
  • 页码:288-299
  • 分类:TP301[自动化与计算机技术—计算机系统结构;自动化与计算机技术—计算机科学与技术]
  • 作者机构:[1]东南大学计算机科学与工程学院,南京210096, [2]江苏科技大学计算机科学与工程学院,江苏镇江212003
  • 相关基金:本课题得到国家自然科学基金项目(60773103,60903161,60903162)、国家“九七三”重点基础研究发展规划项目基金(2010CB328104)、高等学校博士学科点专项科研基金(200802860031)、江苏省自然科学基金重点项目(BK2008030)、江苏省网络与信息安全重点实验室(BM2003201)和计算机网络和信息集成教育部重点实验室(93K-9)资助.
  • 相关项目:可信可控路由机制的研究
中文摘要:

为了解决Petri网的可达性判定问题,提出了一种基于进程验证的可达性判定方法.通过分析Petri网基本进程段子段间偏序关系,该方法提出原子进程段概念,求得原子进程段集及其偏序关系集作为可达性判定的验证对象.基于原网状态方程解向量、原子进程段,T-向量的线性纯整数规划问题解,选取该解中非零分量对应的原子进程段子集作为待验进程段集,选取待验进程段间的偏序关系子集作为待验推理规则集,通过验证是否存在这两个集合上的以初始标识Mo为推导初态、目的标识舰为推导终态的序列而判定(Mo,Ma)是否可达.分析表明该可达性判定算法的时间复杂度是依赖于原子进程段集规模的,最坏情况下不超过变迁集规模.

英文摘要:

In this paper, a process verification based algorithm is proposed to solve the reachability determining problem of Petri net. At first, the definition of atomic process section is introduced based on the partial relation decomposition, and the atomic process section set and the par- tial relation set are sought to act as verified objects in reachability determining. After the solution vector to pure linear nonequivalent expression of state equation solution vector and T-vectors of atomic process sections is calculated, a subset is selected from the atomic process section set with the standard that each element of the subset corresponds to a nonzero component in the solution vector. The partial relation is picked out to form the partial relation subset if it just describes par- tial relation between two elements of the atomic process section subset. If there is a reductive se- quence which explores source marking as start state and target marking as end state, the reachability of Petri net could be concluded. The analysis shows that the time complexity of this determining algorithm depends on the scale of atomic process section set, and is no more than the scale of transition set under the worst condition.

同期刊论文项目
期刊论文 56 会议论文 8 获奖 4 专利 1
期刊论文 48 会议论文 15 专利 3
期刊论文 53 会议论文 15 专利 1
同项目期刊论文