scholarly journals The reachability problem for Petri nets and decision problems for Skolem arithmetic

1980 ◽  
Vol 11 (2) ◽  
pp. 123-143 ◽  
Author(s):  
Egon Börger ◽  
Hans Kleine Büning
1994 ◽  
Vol 05 (03n04) ◽  
pp. 281-292
Author(s):  
HSU-CHUN YEN ◽  
BOW-YAW WANG ◽  
MING-SHANG YANG

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.


2011 ◽  
Vol 22 (04) ◽  
pp. 783-799 ◽  
Author(s):  
MOHAMED FAOUZI ATIG ◽  
PETER HABERMEHL

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.


Author(s):  
Michael Blondin ◽  
Christoph Haase ◽  
Philip Offtermatt

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.


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

Sign in / Sign up

Export Citation Format

Share Document