Reachability for Vector Addition Systems with one zero-test

I'll present a quick summary of the new reachability proof for Vector Addition Systems, designed by J. Leroux (POPL'11). Then, we'll consider a variation of Vector Addition Systems where one counter can be tested for zero and extend the proof of Leroux to our model. This provides an alternate, and hopefully simpler to understand, proof of the reachability problem that was originally proved by Reinhardt.

I'll end the talk by an overview of the various problems that are known decidable for Vector Addition Systems with one zero-test.

This is based on work published in MFCS'11.