Simulation Problems Over One-Counter Nets

Abstract

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.

References in corpus (1)

• Simulation Over One-counter Nets is PSPACE-Complete

Cited by in corpus (3)

• EXPSPACE-hardness of behavioural equivalences of succinct one-counter nets
• Countdown games, and simulation on (succinct) one-counter nets
• The Complexity of Flat Freeze LTL