高级检索

    空标识可再生网的运算和性质分析

    Operating and Analyzing the Reproducibility of Empty Marking Nets

    • 摘要: Lautenbach等人曾给出了一般网空标识可再生 (reproducibility of the empty marking)的充要条件,证明了一个网是空标识可再生的,必须存在含有源(fact)和汇(goal)变迁的非负T-不变,且由该T-不变所组成的变迁外延子网既不含有死锁(siphon),也不含有陷阱(trap).扩展了这个结论,证明了经合成、插入、删除、替换等运算后的网仍保持空标识可再生性.还进一步证明了空标识可再生网的逆网也是空标识可再生的;无环空标识可再生Horn网的T-不变一定可实现;一个含有源和汇变迁的无环P/T网是空标识可再生的,当且仅当其被T-不变所覆盖.这些结论可为复杂的逻辑推理及工作流逻辑网的畅通性检测提供更为有效的方法,最后给出了相应的算法.

       

      Abstract: To reproduce the empty marking, there is a necessary and sufficient condition in which a non-negative T-invariant exists, whose net representations have neither siphons nor traps, containing a positive entry for at least one fact and goal transition. This result is extended and it is proved that the operations of composition, insertion, deletion and substitution do not influence the reproducibility of the empty marking. Moreover, some properties related to the empty marking net are discussed, For example, a net with reproducibility of the empty marking has preserved the reproducibility in its inversed net, and the empty marking in acyclic P/T nets with a positive entry for at least one fact and goal transition is reproducible if and only if the net is covered by T-invariant. In particular, if a Horn-net satisfies all the above conditions and it is acyclic, then the T-invariant is realizable. These theoretical results show that there are interesting connections to other notions, for example, to the forward and backward liveness of the empty marking. On the other hand, there are application oriented aspects of those results. Examples can be found in proving complex logic inference and checking throughness of workflow logic net. Finally its algorithm is proposed.

       

    /

    返回文章
    返回