Flat Petri Nets (Invited Talk)

摘要

Vector addition systems with states (VASS for short), or equivalently Petri nets are one of the most popular formal methods for the representation and the analysis of parallel 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. This paper provides an overview of results about the reachability problem for VASS related to Presburger arithmetic, by presenting 1) a simple algorithm for deciding the reachability problem based on invariants definable in Presburger arithmetic, 2) the class of flat VASS for computing reachability sets in Presburger arithmetic, and 3) complexity results about the reachability problem for flat VASS.