可达性等价于状态方程可满足性的petri网子类

定义了一个petri网子类:PN=(S,T;F,M0),满足条件s∈S→｜·s｜≤1。证明:当目标标识Md>0时,此petri网子类的可达性等价于状态方程Md=M0+ATX的可满足性。同时,当此petri网子类的可达性等价于状态方程可满足性时,可得出如下两点结论:(1)对于满足M0+ATX>0的每个非平凡的非负整数向量X,都■t∈Tx:M0t>;(2)对于满足M0+ATX>0的每个非平凡的非负整数向量X,X都是PN的一个可执行向量。

Class of petri nets with equivalence of reachability and state equation satisfiability

This paper defines a class of petri net PN=(S,T;F,M0) such that s∈S→｜·s｜≤1,and proves that:when every element of the marking Md is great than zero,the reachability from M0 to Md equals to the satisfiability of the state equation Md=M0+ATX.Simultaneously,when the reachability equals to the satisfiability of the state equation,the following conclusions can be drawn:for every vector X such that M0+ATX>0∧X≥0∧X≠0,there exists t∈Tx satisfying M0 t>,and X is an executable vector.