Simulation Problems Over One-Counter Nets

TL;DR

This paper proves that determining strong and weak simulation preorders on one-counter nets, a type of automaton with a non-negative integer counter, is a PSPACE-complete problem, highlighting computational complexity challenges.

Contribution

The paper establishes the PSPACE-completeness of both strong and weak simulation preorders on one-counter nets, providing new complexity results for these models.

Findings

Strong and weak simulation preorders are PSPACE-complete.

Complexity results apply to one-counter nets, a fundamental automaton model.

Highlights computational challenges in analyzing 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.