Computer Science – Logic in Computer Science
Scientific paper
2010-09-06
LMCS 6 (3:22) 2010
Computer Science
Logic in Computer Science
Scientific paper
10.2168/LMCS-6(3:22)2010
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 exclusively based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition. This decomposition is used in this paper to prove that the Parikh images of languages recognized by VASs are semi-pseudo-linear; a class that extends the semi-linear sets, a.k.a. the sets definable in Presburger arithmetic. We provide an application of this result; we prove that a final configuration is not reachable from an initial one if and only if there exists a semi-linear inductive invariant that contains the initial configuration but not the final one. Since we can decide if a Presburger formula denotes an inductive invariant, we deduce that there exist checkable certificates of non-reachability. 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.
No associations
LandOfFree
The General Vector Addition System Reachability Problem by Presburger Inductive Invariants does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with The General Vector Addition System Reachability Problem by Presburger Inductive Invariants, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and The General Vector Addition System Reachability Problem by Presburger Inductive Invariants will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-298437