Ackermann-Hardness for Lossy Counter Machines and Reset Petri Nets

Philippe Schnoebelen

We give a simple construction showing how Lossy Counter Machines (LCM) and Reset Petri Nets (RPN) can weakly compute all the primitive-recursive functions F_n for n=0,1,2,.. in the Grzegorczyck hierarchy as well as their inverses. This entails Ackermann-hardness of reachability and termination, two verification problems known to be decidable, for these models. As an aside, we explain how matching complexity upper bounds can be easily obtained with the length function theorem for bad sequences in well-quasi-orders.