Directed Reachability for Infinite-State Systems.

摘要: Numerous tasks in program analysis and synthesis reduce to deciding reachability possibly infinite graphs such as those induced by Petri nets. However, the net problem has recently been shown require non-elementary time, which raises questions about practical applicability of nets target models. In this paper, we introduce a novel approach for efficiently semi-deciding practice. Our key insight is that computationally lightweight over-approximations can be used distance oracles classical graph exploration algorithms A* greedy best-first search. We provide evaluate prototype implementation our outperforms existing state-of-the-art tools, sometimes orders magnitude, also competitive with domain-specific tools on benchmarks coming from concurrent analysis.