论文标题
无限状态系统的定向可达性
Directed Reachability for Infinite-State Systems
论文作者
论文摘要
程序分析和综合中的许多任务都减少了可能无限图的可及性，例如培养皿网络。但是，最近已证明Petri净到达性问题需要非元素时间，这引发了有关Petri Nets作为目标模型的实际适用性的问题。在本文中，我们介绍了一种新颖的方法，用于在实践中有效地半偏向培养皿的可及性问题。我们的关键见解是，在经典图形探索算法（例如A*和贪婪的最佳优点搜索）中，Petri Nets的计算轻量级过度介绍可用作距离甲壳。我们提供和评估我们方法的原型实现，该实现优于现有的最先进工具，有时是按数量级的订单，并且与来自程序合成和并发程序分析的基准分析的域特异性工具也具有竞争力。
Numerous tasks in program analysis and synthesis reduce to deciding reachability in possibly infinite graphs such as those induced by Petri nets. However, the Petri net reachability problem has recently been shown to require non-elementary time, which raises questions about the practical applicability of Petri nets as target models. In this paper, we introduce a novel approach for efficiently semi-deciding the reachability problem for Petri nets in practice. Our key insight is that computationally lightweight over-approximations of Petri nets can be used as distance oracles in classical graph exploration algorithms such as A* and greedy best-first search. We provide and evaluate a prototype implementation of our approach that outperforms existing state-of-the-art tools, sometimes by orders of magnitude, and which is also competitive with domain-specific tools on benchmarks coming from program synthesis and concurrent program analysis.
