基于T-不变量消除的Petri网合法变迁引发序列判定算法

摘要：

Petri网的合法变迁引发序列问题(LFS)是其可达性问题的子问题。前人在LFS判定时常因判定算法的指数级时空复杂度或算法难以推广至一般Petri网而受限.因此,基于Petri网T-不变量支集变迁与可达图有向环路上标注变迁的对应关系,综合应用线性代数与可达树分析,原LFS判定被缩减为以基础向量为发生数向量的LFSb判定.通过两棵可达树(分别以原网、初始标识;逆网、目的标识为根)层序轮流构造同时比较当前叶节点层中的标识,若算法终止前有相同标识出现,则LFSb(LFS)判定成功;反之,LFS判定失败.分析表明,算法的时间复杂度为多项式级别的,且适用于一般Petri网的LFS判定.

关键词： Petri网 可达性 合法变迁引发序列 T-不变量消除

作者: 于枫 罗军舟 李伟

作者单位: 东南大学,计算机科学与工程学院,江苏,南京,210096;江苏科技大学电子信息学院,江苏,镇江,212003 东南大学,计算机科学与工程学院,江苏,南京,210096

会议类型: 国内会议

会议名称: 第十六届全国网络与数据通信学术会议(NDCC2008)

会议地点: 南京

会议语种:中文

页码: 522-527

在线出版日期: 2008-11-10（万方平台首次上网日期，不代表论文的发表时间）