Directed reachability for infinite-state systems

DOI10.1007/978-3-030-72013-1_1MaRDI QIDQ2233488zbMATH OpenOpenAlexFDO

Authors Michael Blondin, Christoph Haase, Philip Offtermatt

Publication date 18 October 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2010.07912

shortest paths model checking reachability Petri nets

Graph theory (including graph drawing) in computer science (68R10) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: 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.

Recommendations

Cites work

Cited in

(7)

This page was built for publication: Directed reachability for infinite-state systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233488)