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