Verification column

Notwithstanding the rapid recent progress in settling the very high computational complexity of the reachability problem, VASS (also known as Petri nets) remain an intriguing model of concurrency with extensive significance for verification and synthesis. In this engaging article, Tony introduces us to asymptotic analysis of VASS, showing that many relevant problems have attractive complexities, and concluding with several inviting directions for further investigations.