论文标题
最佳标签分裂将LT嵌入任意Petri Net可及性图中是NP完整的
Optimal Label Splitting for Embedding an LTS into an arbitrary Petri Net Reachability Graph is NP-complete
论文作者
论文摘要
对于给定标记的过渡系统(LTS),合成是找到具有同构可及性图的未标记的培养皿网的任务。即使仅要求将嵌入到可及图中而不是同构中,也不能保证解决方案。在这种情况下,标签拆分是一种选项,即LT的重新标记边缘,因此标记的边缘不同。通过适当的标签分裂,我们始终可以为合成或嵌入问题提供解决方案。使用标签拆分,我们可以用预期的bahaviour构建标有培养皿网(例如将给定的LT嵌入其可及性图中)。由于标记的Petri Net可以具有大量的过渡,因此可能需要优化,从而限制了标签拆分产生的标签数量。我们表明,这样的限制将使问题从在多项式时间内的解决方案转变为NP完整问题。
For a given labelled transition system (LTS), synthesis is the task to find an unlabelled Petri net with an isomorphic reachability graph. Even when just demanding an embedding into a reachability graph instead of an isomorphism, a solution is not guaranteed. In such a case, label splitting is an option, i.e. relabelling edges of the LTS such that differently labelled edges remain different. With an appropriate label splitting, we can always obtain a solution for the synthesis or embedding problem. Using the label splitting, we can construct a labelled Petri net with the intended bahaviour (e.g. embedding the given LTS in its reachability graph). As the labelled Petri net can have a large number of transitions, an optimisation may be desired, limiting the number of labels produced by the label splitting. We show that such a limitation will turn the problem from being solvable in polynomial time into an NP-complete problem.