为Petri-Net模型标记器添加有用功能的建议
Proposal for Adding Useful Features to Petri-Net Model Checkers
摘要：
长期存在的问题提出的解决方案的自动分解的Petri网到并发进程，以及在格勒诺布尔开发的方法的自动转换的安全Petri网NUPN（嵌套单元Petri网），需要一定的性能计算的Petri网。我们注意到，虽然这些属性在理论上是有趣的，实际上是有用的，他们目前还没有实现在主流的Petri网工具。考虑到这些属性将为工具开发人员开辟富有成效的研究方向，也为模型检验竞赛开辟新的视角。
英文摘要：
Solutions proposed for the longstanding problem of automatic decomposition of Petri nets into concurrent processes, as well as methods developed in Grenoble for the automatic conversion of safe Petri nets to NUPNs (Nested-Unit Petri Nets), require certain properties to be computed on Petri nets. We notice that, although these properties are theoretically interesting and practically useful, they are not currently implemented in mainstream Petri net tools. Taking into account such properties would open fruitful research directions for tool developers, and new perspectives for the Model Checking Contest as well.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
