可达性与状态方程可满足性等价的两个Petri网子类

可达性是Petri网最基本最重要的动态性质之一,但一般Petri网的可达性判定问题至少具有指数空间复杂度,且目前尚无有效的判定算法。不过,存在某些Petri网子类,其可达性判定问题要相对简单,寻找这样的Petri网子类具有重要意义。为此,提出极小陷阱回路网与后向回路网的概念,并证明了初始标识下不含空极小回路的这两个Petri网子类,其可达性判定问题等价于状态方程的可满足性问题。

Two classes of Petri Nets with Reachability Equivalent to State Equation Satisfiability

Reachability is one of the most basic and important dynamic properties of Petri nets. But the reachability decidability problem has at least exponential space complexity and no effective algorithm is found by now. However, there exist some special Petri nets the reachability problem of which is easiliy to be decided. And it has great significance to find such Petri nets subclasses. For this reason, the definitions of minimal-trap-circuit Petri net and backward-circuit Petri net are provided in this paper. It is pointed out that the reachability problem of these two kinds of Petri nets subclasses is equivalent to the satisfiability of state equation if no token-freee minimal circuit exists under the initial marking.