zbMATH — the first resource for mathematics

Mixing coverability and reachability to analyze VASS with one zero-test. (English) Zbl 1274.68230
van Leeuwen, Jan (ed.) et al., SOFSEM 2010: Theory and practice of computer science. 36th conference on current trends in theory and practice of computer science, Špindlerův Mlýn, Czech Republic, January 23–29, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-11265-2/pbk). Lecture Notes in Computer Science 5901, 394-406 (2010).
Summary: 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.
For the entire collection see [Zbl 1180.68007].

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI