scholarly journals The General Vector Addition System Reachability Problem by Presburger Inductive Invariants

Author(s):  
Jérôme Leroux
10.29007/bnx2 ◽  
2018 ◽  
Author(s):  
Jerome Leroux

The reachability problem for Vector Addition Systems (VASs) is a central problem of net theory. The general problem is known to be decidable by algorithms based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition (KLMTS decomposition). Recently from this decomposition, we deduced that a final configuration is not reachable from an initial one if and only if there exists a Presburger inductive invariant that contains the initial configuration but not the final one. Since we can decide if a Preburger formula denotes an inductive invariant, we deduce from this result that there exist checkable certificates of non-reachability in the Presburger arithmetic. In particular, there exists a simple algorithm for deciding the general VAS reachability problem based on two semi-algorithms. A first one that tries to prove the reachability by enumerating finite sequences of actions and a second one that tries to prove the non-reachability by enumerating Presburger formulas. In another recent paper we provided the first proof of the VAS reachability problem that is not based on the KLMST decomposition. The proof is based on the notion of production relations that directly proves the existence of Presburger inductive invariants. In this paper we propose new intermediate results simplifying a bit more this last proof.


2005 ◽  
Vol 16 (04) ◽  
pp. 683-705 ◽  
Author(s):  
OSCAR H. IBARRA ◽  
HSU-CHUN YEN ◽  
ZHE DANG

We consider the following definition (different from the standard definition in the literature) of "maximal parallelism" in the application of evolution rules in a P system G: Let R = {r1, …rk} be the set of (distinct) rules in the system. G operates in maximally parallel mode if at each step of the computation, a maximal subset of R is applied, and at most one instance of any rule is used at every step (thus at most k rules are applicable at any step). We refer to this system as a maximally parallel system. We look at the computing power of P systems under three semantics of parallelism. For a positive integer n ≤ k, define: n-Max-Parallel: At each step, nondeterministically select a maximal subset of at most n rules in R to apply (this implies that no larger subset is applicable). ≤ n-Parallel: At each step, nondeterministically select any subset of at most n rules in R to apply. n-Parallel: At each step, nondeterministically select any subset of exactly n rules in R to apply. In all three cases, if any rule in the subset selected is not applicable, then the whole subset is not applicable. When n = 1, the three semantics reduce to the Sequential mode. We focus on two popular models of P systems: multi-membrane catalytic systems and communicating P systems. We show that for these systems, n-Max-Parallel mode is strictly more powerful than any of the following three modes: Sequential, ≤ n-Parallel, or n-Parallel. For example, it follows from the result in [9] that a maximally parallel communicating P system is universal for n = 2. However, under the three limited modes of parallelism, the system is equivalent to a vector addition system, which is known to only define a recursive set. These generalize and refine the results for the case of 1-membrane systems recently reported in [3]. Some of the present results are rather surprising. For example, we show that a Sequential 1-membrane communicating P system can only generate a semilinear set, whereas with k membranes, it is equivalent to a vector addition system for any k ≥ 2 (thus the hierarchy collapses at 2 membranes - a rare collapsing result for nonuniversal P systems). We also give another proof (using vector addition systems) of the known result [8] that a 1-membrane catalytic system with only 3 catalysts and (non-prioritized) catalytic rules operating under 3-Max-Parallel mode can simulate any 2-counter machine M. Unlike in [8], our catalytic system needs only a fixed number of noncatalysts, independent of M. A simple cooperative system (SCO) is a P system where the only rules allowed are of the form a → v or of the form aa → v, where a is a symbol and v is a (possibly null) string of symbols not containing a. We show that a 9-Max-Parallel 1-membrane SCO is universal.


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.


Sign in / Sign up

Export Citation Format

Share Document