Sciweavers

Share
SOFSEM
2010
Springer

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

10 years 6 months ago
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.
Alain Finkel, Arnaud Sangnier
Added 17 Mar 2010
Updated 17 Mar 2010
Type Conference
Year 2010
Where SOFSEM
Authors Alain Finkel, Arnaud Sangnier
Comments (0)
books