Litcius/Paper detail

Reachability in Vector Addition Systems is Ackermann-complete

Wojciech Czerwiński, Lukasz Orlikowski

202267 citationsDOI

Abstract

Vector Addition Systems and equivalent Petri nets are a well established models of concurrency. The central algorithmic problem for Vector Addition Systems with a long research history is the reachability problem asking whether there exists a run from one given configuration to another. We settle its complexity to be Ackermann-complete thus closing the problem open for 45 years. In particular we prove that the problem is <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$\mathcal{F}_{k}$</tex> -hard for Vector Addition Systems with States in dimension 6k, where <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$\mathcal{F}_{k}$</tex> is the <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$k$</tex> -th complexity class from the hierarchy of fast-growing complexity classes.

Topics & Concepts

Ackermann functionReachabilityPetri netComputer scienceDiscrete mathematicsClass (philosophy)CombinatoricsTheoretical computer scienceMathematicsAlgebra over a fieldAlgorithmArtificial intelligencePure mathematicsInverseGeometryPetri Nets in System ModelingFormal Methods in Verificationsemigroups and automata theory