Petri nets is a fundamental model in the area of formal verification. It is popular in both theoretical study and application. For the analysis of algorithmic properties of Petri nets, they are often equivalently viewed as vector addition systems. This survey gives a comprehensive review of the recent achievements in this area. First, formal definitions of the vector addition systems and their key verification problems are provided with emphasis on the discussion about reachability problem, including the latest results and the main proof techniques. Then the development on the case where the dimension is a constant number rather than a variable is summarized along with some key theorems which are fundamental to the current complexity results. Furthermore, as some important variants of vector addition systems have been proposed in recent years, a brief introduction is given to the motivation and definitions of some of the most representative ones, and the latest results on verification relating to these models. In addition, possible future work are highlighted at the end of each section.