论文标题
立即观察培养皿网的平坦度和复杂性
Flatness and Complexity of Immediate Observation Petri Nets
论文作者
论文摘要
在上一篇论文中，我们引入了立即观察（IO）培养皿网，这是对人口方案和酶学化学网络的研究的一种兴趣。在本文的第一部分中，我们表明IO网是全球平坦的，因此可以使用加速技术（如FAST）进行有效的符号模型检查工具来检查其安全性能。在第二部分中，我们研究了分支IO网（生物网），其过渡可以创建令牌。生物网同时扩展了IO网和无通信网，也称为BPP网，这是一个广泛研究的类。我们表明，虽然生物网不再是全球平坦的，而且它们的可及标记可能是非摩擦性的，但它们仍然是本地平坦的。结果，Pspace中的生物网的覆盖性和可及性问题，甚至是某些设定的参数化版本。这使得生物网成为具有非摩擦性可及性关系的第一个自然净类类别，其可及性问题比一般的培养皿网络更简单。
In a previous paper we introduced immediate observation (IO) Petri nets, a class of interest in the study of population protocols and enzymatic chemical networks. In the first part of this paper we show that IO nets are globally flat, and so their safety properties can be checked by efficient symbolic model checking tools using acceleration techniques, like FAST. In the second part we study Branching IO nets (BIO nets), whose transitions can create tokens. BIO nets extend both IO nets and communication-free nets, also called BPP nets, a widely studied class. We show that, while BIO nets are no longer globally flat, and their sets of reachable markings may be non-semilinear, they are still locally flat. As a consequence, the coverability and reachability problem for BIO nets, and even a certain set-parameterized version of them, are in PSPACE. This makes BIO nets the first natural net class with non-semilinear reachability relation for which the reachability problem is provably simpler than for general Petri nets.
