peti分析报告.docVIP

Decidability analysis of some classes of extended function Petri net （某些类功能拓展的petri网的可决定性分析） 主题：某些有结构限制的功能拓展petri网的活性和可达性分析，活性是验证系统是否存在局部死锁，可达性是验证系统能否由初始状态到达目标状态。 一个功能拓展的petri网模型： 由Fig.1可知，库所p1不会影响t2的激发，当t2被激发时，库所p1里的令牌（或资源）将被全部带走，相当于库所p1被重置了，所以从p1到t2的有向弧称为重置弧。由h(M)=2M(p2)知，从p2到t2 是禁止弧，只要库所p2里有令牌，t2就不能被激发，所以可以用条件W(p,t)=2M(p)来表示禁止弧。 令x为EFPN Σ =(P, T, F, W, M0)的库所p或变迁t， •x = {y|(y, x) ∈ F}为x的输入弧的集合，为x的输出弧的集合。 扩展的自由选择EFC (extended free choice net)网的定义：对所有的库所满足 p1, p2 ∈P, p1 • ∩ p2 • = ∅ 意味着 p1 • = p2 •。 扩展的非对称选择petri网EAC net(extended asymmetric choice petri net)的定义：对所有的p1 , p2 ∈ P, 由p1 • ∩ p2 • = ∅ 可得p1 • ⊆p2 • 或 p1 • ⊇ p2 •。 准普通扩展功能petri网（Quasi ordinary EFPN）:满足一下三个条件 For any marking M ≥ 0 and for any arc a from a place to a transition, W(a)(M) ≥ 1 thanks to max operations involving the value 1. Both of the transitions t1 and t2 are enabled if and only if M(p1) ≥ 1 and M(p2) ≥ 1. When t1 fires, it removes all tokens from both of p1 and p2 and puts one token to p3. When t2 fires, it removes min{M(p1 ), M(p2)} tokens from p1 and p2 and puts the same number of tokens to p3. 准等冲突的功能拓展petri网的定义： （其中w(p)其是库所p的输出权函数） 结论：Liveness is decidable if it is quasi ordinary and has the EFC structure. On the other hand, liveness is undecidable for extended function net if either (1) it is quasi ordinary and has asymmetric choice structure or (2) it is quasi equal conflict and has the EFC structure.Reachability is undecidable for all of above classes.（只有具有自由选择结构的准普通petri网的活性是可决定的。具有非对称结构的准普通petri网或者是具有自由选择结构的准等冲突petri网的活性是不可决定的。上面提及的petri网的可达性都是不可决定的。） 研究方向：其他含有抑制弧的无界子类petri网的可决定性问题。