Mixing Coverability and Reachability to Analyze VASS with One Zero-Test

We study Vector Addition Systems with States (VASS) extended in such a way that one of the manipulated integer variables can be tested to zero. For this class of system, it has been proved that the reachability problem is decidable. We prove here that boundedness, termination and reversal-boundedness are decidable for VASS with one zero-test. To decide reversal-boundedness, we provide an original method which mixes both the construction of the coverability graph for VASS and the computation of the reachability set of reversal-bounded counter machines. The same construction can be slightly adapted to decide boundedness and hence termination.

• Type: Conference
• Year: 2010
• Where: SOFSEM
• Authors: Alain Finkel, Arnaud Sangnier
• Keywords: Reachability Problem, Reachability Set, SOFSEM 2010, Theoretical Computer Science, Vector Addition Systems