Decidability of reachability in vector addition systems (Preliminary Version) 论文

摘要

A convincing proof of the decidability of reachability in vector addition systems is presented. No drastically new ideas beyond those in Sacerdote and Tenney, and Mayr are made use of. The complicated tree constructions in the earlier proofs are completely eliminated.