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

• 作 者: 于枫 罗军舟 李伟
• 机 构: 东南大学计算机科学与工程学院,江苏科技大学电子信息学院
• 出 处: 解放军理工大学学报：自然科学版
• 发表日期: 2008年5期
• 关键词: PETRI网 可达性 合法变迁引发序列 T-不变量 Petri net reachability legal firing transition seque
• 基金项目: 国家自然科学基金资助项目（90604004）,江苏省自然科学基金资助项目（BK2007708）.

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