When Reachability Meets Grzegorczyk
Jérôme Leroux · 2020
Vector addition systems with states, or equivalently vector addition systems, or Petri nets are a long established model of concurrency with extensive applications in modelling and analysis of hardware, software and database systems, as well as chemical, biological and business processes. The central algorithmic problem is reachability: whether from a given initial configuration there exists a sequence of valid execution steps that reaches a given final configuration. The complexity of the problem has remained unsettled since the 1960s, and it is one of the most prominent open questions in the theory of computation.