论文标题
避免厄运:在培养皿网中查找悬崖边缘配置
Avoid One's Doom: Finding Cliff-Edge Configurations in Petri Nets
论文作者
论文摘要
分析并发系统的一个至关重要的问题是确定其长期行为,尤其是其演变中是否存在不可逆转的选择,导致无法返回其他部分的一部分可达性空间。我们以前的工作在安全培养皿网的统一框架中施加了这个问题,为识别吸引子的技术提供了技术,即可达性空间的终端组成部分,我们希望确定其吸引力的盆地。在这里,我们为安全培养皿网的情况提供了一种解决方案。我们的算法使用NET展开,并提供了充当悬崖边缘的所有系统配置(并发执行)的地图,即这些配置的最大扩展位于某些被认为是致命的盆地中。事实证明,计算仅需要相对较小的前缀,只有Esparza完整前缀的深度是两倍。
A crucial question in analyzing a concurrent system is to determine its long-run behaviour, and in particular, whether there are irreversible choices in its evolution, leading into parts of the reachability space from which there is no return to other parts. Casting this problem in the unifying framework of safe Petri nets, our previous work has provided techniques for identifying attractors, i.e. terminal strongly connected components of the reachability space, whose attraction basins we wish to determine. Here, we provide a solution for the case of safe Petri nets. Our algorithm uses net unfoldings and provides a map of all of the system's configurations (concurrent executions) that act as cliff-edges, i.e. any maximal extension for those configurations lies in some basin that is considered fatal. The computation turns out to require only a relatively small prefix of the unfolding, just twice the depth of Esparza's complete prefix.