Presynthesis of bounded choice-free or fork-attribution nets
Presynthesis of bounded choice-free or fork-attribution nets
复制标题
DOI：
10.1016/j.ic.2019.104482
复制
发表时间：
2020-04-01
影响因子：
1
通讯作者：
Wimmel, Harro
中科院分区：
文献类型：
--
作者：
Wimmel, Harro
一个Petri网被称为fork-attribution，如果它是choice-free的（每个位置的唯一输出转移）和join-free的（每个转移的唯一输入位置）。合成尝试，对于一个给定的（有限的）标记的转移系统（LTS），找到一个（未标记的）Petri网与同构的可达图。合成通常需要解决大量的不等式系统，这使得它非常昂贵。在预合成中，我们利用一些类的Petri网的共同的必要性质。如果任何一个性质不成立，我们可以直接放弃LTS，它不可能是我们类中的Petri网的可达图。这也允许实现给出有意义的响应，而不是仅仅告诉用户某些不等式系统是不可解的。如果所有的性质都成立，我们就可以得到更多的信息，从而简化待解的不等式组。在本文中，我们从理论上增强，并调整算法的预合成策略已经知道的选择自由网分叉属性网。(C)2019爱思唯尔公司All rights reserved.
A Petri net is called fork-attribution if it is choice-free (a unique output transition for each place) and join-free (a unique input place for each transition). Synthesis tries, for a given (finite) labelled transition system (LTS), to find an (unlabelled) Petri net with an isomorphic reachability graph. Synthesis often requires a large set of inequality systems to be solved, making it quite costly. In presynthesis we exploit common necessary properties of some class of Petri nets. If any of the properties do not hold, we can directly dismiss the LTS, it cannot be the reachability graph of a Petri net from our class. This also allows an implementation to give a meaningful response instead of just telling the user that some inequality system is unsolvable. If all properties hold, we may gain additional information that can simplify the inequality systems to be solved. In this paper, we enhance theoretically, and tune algorithmically a presynthesis strategy already known for choice-free nets to fork-attribution nets. (C) 2019 Elsevier Inc. All rights reserved.