scholarly journals The Reachability Problem for Petri Nets Is Not Elementary

2021 ◽  
Vol 68 (1) ◽  
pp. 1-28
Author(s):  
Wojciech Czerwiński ◽  
Sławomir Lasota ◽  
Ranko Lazić ◽  
JÉrôme Leroux ◽  
Filip Mazowiecki
Keyword(s):  
Petri Nets ◽  
Reachability Problem

SOME COMPLEXITY RESULTS FOR RINGS OF PETRI NETS

1994 ◽  
Vol 05 (03n04) ◽  
pp. 281-292
Author(s):  
HSU-CHUN YEN ◽  
BOW-YAW WANG ◽  
MING-SHANG YANG
Keyword(s):  
Petri Nets ◽  
State Machines ◽  
Slight Improvement ◽  
Reachability Problem ◽  
Encoding Scheme ◽  
N Cycle ◽  
Vector Addition ◽  
Finite State ◽  
Boundedness Problem ◽  
Compare And Contrast

We define a subclass of Petri nets called m–state n–cycle Petri nets, each of which can be thought of as a ring of n bounded (by m states) Petri nets using n potentially unbounded places as joins. Let Ring(n, l, m) be the class of m–state n–cycle Petri nets in which the largest integer mentioned can be represented in l bits (when the standard binary encoding scheme is used). As it turns out, both the reachability problem and the boundedness problem can be decided in O(n(l+log m)) nondeterministic space. Our results provide a slight improvement over previous results for the so-called cyclic communicating finite state machines. We also compare and contrast our results with that of VASS(n, l, s), which represents the class of n-dimensional s-state vector addition systems with states where the largest integer mentioned can be described in l bits.

scholarly journals ON YEN'S PATH LOGIC FOR PETRI NETS

2011 ◽  
Vol 22 (04) ◽  
pp. 783-799 ◽  
Author(s):  
MOHAMED FAOUZI ATIG ◽  
PETER HABERMEHL
Keyword(s):  
Petri Nets ◽  
Satisfiability Problem ◽  
Reachability Problem ◽  
Almost All

In [19], Yen defines a class of formulas for paths in Petri nets and claims that its satisfiability problem is EXPSPACE-complete. In this paper, we show that in fact the satisfiability problem for this class of formulas is as hard as the reachability problem for Petri nets. Moreover, we salvage almost all of Yen's results by defining a fragment of this class of formulas for which the satisfiability problem is EXPSPACE-complete by adapting his proof.

scholarly journals Directed Reachability for Infinite-State Systems

2021 ◽  
pp. 3-23
Author(s):  
Michael Blondin ◽  
Christoph Haase ◽  
Philip Offtermatt
Keyword(s):  
Petri Nets ◽  
Program Analysis ◽  
Infinite Graphs ◽  
Reachability Problem ◽  
Graph Exploration ◽  
Concurrent Program ◽  
Domain Specific ◽  
Novel Approach ◽  
Distance Oracles ◽  
Analysis And Synthesis

AbstractNumerous 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 $$\mathsf {A}^{*}$$ 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.

Sign in / Sign up

Export Citation Format

Share Document