Countdown games, and simulation on (succinct) one-counter nets

TL;DR

This paper establishes that simulation preorder on succinct one-counter nets is EXPSPACE-complete, resolving an open complexity question and providing new proofs and algorithms for related reachability and countdown games.

Contribution

It proves EXPSPACE-completeness of simulation preorder on succinct one-counter nets and offers simplified proofs and algorithms for related problems.

Findings

Simulation preorder is EXPSPACE-complete.

A new simplified proof of the belt theorem is provided.

Polynomial-space algorithm for non-succinct one-counter nets is developed.

Abstract

We answer an open complexity question by Hofman, Lasota, Mayr, Totzke (LMCS 2016) for simulation preorder on the class of succinct one-counter nets (i.e., one-counter automata with no zero tests where counter increments and decrements are integers written in binary); the problem was known to be PSPACE-hard and in EXPSPACE. We show that all relations between bisimulation equivalence and simulation preorder are EXPSPACE-hard for these nets; simulation preorder is thus EXPSPACE-complete. The result is proven by a reduction from reachability games whose EXPSPACE-completeness in the case of succinct one-counter nets was shown by Hunter (RP 2015), by using other results. We also provide a direct self-contained EXPSPACE-completeness proof for a special case of such reachability games, namely for a modification of countdown games that were shown EXPTIME-complete by Jurdzinski, Sproston, Laroussinie (LMCS 2008); in our modification the initial counter value is not given but is freely chosen by the first player. We also present an alternative proof for the upper bound by Hofman et al. In particular, we give a new simplified proof of the belt theorem that yields a simple graphic presentation of simulation preorder on (non-succinct) one-counter nets and leads to a polynomial-space algorithm (which is trivially extended to an exponential-space algorithm for succinct one-counter nets).