Directed reachability for infinite-state systems

DOI10.1007/978-3-030-72013-1_1zbMATH Open1474.68202arXiv2010.07912OpenAlexW3145100375MaRDI QIDQ2233488FDOQ2233488

Michael Blondin, Philip Offtermatt, Christoph Haase

Publication date: 18 October 2021

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.

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

Recommendations

• Applications and Theory of Petri Nets 2004
• Directed Unfolding of Petri Nets
• Compositional reachability in Petri nets
• The reachability problem for Petri nets is not elementary
• The Reachability Problem for Petri Nets Is Not Elementary

zbMATH Keywords

shortest pathsmodel checkingreachabilityPetri nets

Mathematics Subject Classification ID

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)

Cites Work

• Component-based synthesis for complex APIs
• Model checking and abstraction to the aid of parameterized systems (a survey)
• A Petri net approach to the study of persistence in chemical reaction networks
• Reasoning about systems with many processes
• Title not available (Why is that?)
• The covering and boundedness problems for vector addition systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• A structure to decide reachability in Petri nets
• Complexity analysis of continuous Petri nets
• Complexity of some problems in Petri nets
• Title not available (Why is that?)
• Title not available (Why is that?)
• Some decision problems related to the reachability problem for Petri nets
• Demystifying Reachability in Vector Addition Systems
• Verification of population protocols
• Survey on Directed Model Checking
• Structural Counter Abstraction
• Title not available (Why is that?)
• The reachability problem for Petri nets is not elementary
• Parameterized complexity and approximability of coverability problems in weighted Petri nets
• The Logical View on Continuous Petri Nets
• Context-free commutative grammars with integer counters and resets
• Occam's razor applied to the Petri net coverability problem
• Unbounded-Thread Program Verification using Thread-State Equations
• An SMT-Based Approach to Coverability Analysis
• Continuous reachability for unordered data Petri nets is in PTime
• Title not available (Why is that?)

Cited In (5)

• A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking
• Coverability in 2-VASS with one unary counter is in NP
• Lower bounds for the reachability problem in fixed dimensional VASSes
• Fast termination and workflow nets
• Property directed reachability for generalized Petri nets

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)