Simultaneous Petri Net Synthesis
Simultaneous Petri Net Synthesis
复制标题
DOI：
10.7561/sacs.2018.2.199
复制
发表时间：
2018-01-01
影响因子：
0.9
通讯作者：
Wimmel, Harro
中科院分区：
文献类型：
--
作者：
Best, Eike;Devillers, Raymond;Wimmel, Harro
研究了给定一个标号变迁系统TS，能否找到一个初始标记为M-0且(N，M-0)的可达图与TS同构的Petri网N的问题。在此之前可能会有一个预合成阶段，该阶段将快速拒绝格式错误的转换系统(并给出失败的结构原因)，否则将构建正确合成所需的数据结构。最后一个阶段是通过解线性不等式组来进行的，但由于不太透明的原因，它仍然可能失败。在本文中，我们考虑了一个推广的问题。一个有限变迁系统集{TS1，…，TSM}称为同时可解的，如果存在一个具有多个初始标记{M-01，…，M-0m}的单一的Petri网N，使得对于每个i=1，…，m，(N，M-0i)的可达图与TSI同构。重点将集中在无选择网，即没有结构选择的网，并探索如何将以前发表的有界无选择网的预合成和适当合成的有效算法推广到这种多标记网的同时预合成和合成。同时，通过引入新的结构检查，加强对单一过渡制度的无选择预合成。
Petri net synthesis deals with the problem whether, given a labelled transition system TS, one can find a Petri net N with an initial marking M-0 such that the reachability graph of (N, M-0) is isomorphic to TS. This may be preceded by a pre-synthesis phase that will quickly reject ill-formed transition systems (and give structural reasons for the failure) and otherwise build data structures needed by the proper synthesis. The last phase proceeds by solving systems of linear inequalities, and may still fail but for less transparent reasons. In this paper, we consider an extended problem. A finite set of transition systems {TS1, ... , TSm} shall be called simultaneously Petri net solvable if there is a single Petri net N with several initial markings {M-01, ... , M-0m}, such that for every i = 1, ... , m, the reachability graph of (N, M-0i) is isomorphic to TSi. The focus will be on choice-free nets, that is, nets without structural choices, and we explore how previously published efficient algorithms for the pre-synthesis and proper synthesis of bounded and choice-free Petri nets can be generalised for the simultaneous pre-synthesis and synthesis of such multi-marked nets. At the same time, the choice-free pre-synthesis of a single transition system shall be strengthened by introducing new structural checks.