EXPSPACE-hardness of behavioural equivalences of succinct one-counter nets

TL;DR

This paper establishes that the problems of simulation preorder and bisimulation equivalence for succinct one-counter nets are EXPSPACE-complete, providing new complexity results and a direct proof for reachability games.

Contribution

It provides a direct EXPSPACE-hardness proof for reachability games on succinct one-counter nets and reduces these to (bi)simulation games, clarifying their computational complexity.

Findings

Simulation preorder and bisimulation equivalence are EXPSPACE-complete.

A new direct EXPSPACE-hardness proof for reachability games is presented.

Reduction from reachability games to (bi)simulation games is demonstrated.

Abstract

We note that the remarkable EXPSPACE-hardness result in [G\"oller, Haase, Ouaknine, Worrell, ICALP 2010] ([GHOW10] for short) allows us to answer an open complexity question for simulation preorder of succinct one counter nets (i.e., one counter automata with no zero tests where counter increments and decrements are integers written in binary). This problem, as well as bisimulation equivalence, turn out to be EXPSPACE-complete. The technique of [GHOW10] was referred to by Hunter [RP 2015] for deriving EXPSPACE-hardness of reachability games on succinct one-counter nets. We first give a direct self-contained EXPSPACE-hardness proof for such reachability games (by adjusting a known PSPACE-hardness proof for emptiness of alternating finite automata with one-letter alphabet); then we reduce reachability games to (bi)simulation games by using a standard "defender-choice" technique.