EXPSPACE-hardness of behavioural equivalences of succinct one-counter nets
Petr Jancar, Petr Osicka, Zdenek Sawa

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Software Testing and Debugging Techniques
