Authors: Piotr Hofman ; Slawomir Lasota ; Richard Mayr ; Patrick Totzke

One-counter nets (OCN) are finite automata equipped with a counter that can store non-negative integer values, and that cannot be tested for zero. Equivalently, these are exactly 1-dimensional vector addition systems with states. We show that both strong and weak simulation preorder on OCN are PSPACE-complete.

• 68Q17 - Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
• 68Q85 - Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)