Relabelling LTS for Petri Net Synthesis via Solving Separation Problems
Relabelling LTS for Petri Net Synthesis via Solving Separation Problems
复制标题
DOI：
10.1007/978-3-662-60651-3_9
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
U. Schlachter;Harro Wimmel
中科院分区：
文献类型：
--
作者：
U. Schlachter;Harro Wimmel
Petri 网综合涉及寻找一个未标记的 Petri 网，其可达性图与给定的通常有限的标记转换系统 (LTS) 同构。如果综合问题没有解决方案，我们使用标签分割。这意味着我们重新标记边缘，直到 LTS 变得可综合。我们获得一个未标记的 Petri 网和一个重新标记函数，它们一起形成一个具有原始预期行为的标记 Petri 网。通过仔细选择要重新标记的边，我们希望保持 LTS 的字母表和构建的 Petri 网尽可能小。即使是近似算法也很难获得最佳的重新标记。使用区域理论，我们开发了基于两种分离问题的多项式启发式方法。这些要么需要不同的 LTS 状态的不同 Petri 网标记，要么需要 LTS 中边缘的存在与状态标记下的转换激活之间的对应关系。如果任何分离问题无法解决，则需要在 LTS 中重新标记边缘。我们展示了选择这些边缘的有效方法。
Petri net synthesis deals with finding an unlabelled Petri net with a reachability graph isomorphic to a given usually finite labelled transition system (LTS). If there is no solution for a synthesis problem, we use label splitting. This means that we relabel edges until the LTS becomes synthesisable. We obtain an unlabelled Petri net and a relabelling function, which together form a labelled Petri net with the original, intended behaviour. By careful selection of the edges to relabel we hope to keep the alphabet of the LTS and the constructed Petri net as small as possible. Even approximation algorithms, not yielding an optimal relabelling, are hard to come by. Using region theory, we develop a polynomial heuristic based on two kinds of separation problems. These either demand distinct Petri net markings for distinct LTS states or a correspondence between the existence of an edge in the LTS and the activation of a transition under the state’s marking. If any separation problem is not solvable, relabelling of edges in the LTS becomes necessary. We show efficient ways to choose those edges.