一句话：证明 succinct 单计数器网上模拟前序为 EXPSPACE 完全，并给出倒计时游戏变体的自包含证明。
本文解决 Hofman 等人（LMCS 2016）关于 succinct 单计数器网上模拟前序的开放复杂度问题。该模型是不含零测试、计数器增减为二进制整数的单计数器自动机，此前仅知 PSPACE-hard 且属于 EXPSPACE。作者证明互模拟等价与模拟前序之间的所有关系均为 EXPSPACE-hard，从而模拟前序达到 EXPSPACE 完全。证明从 succinct 单计数器网上的可达性游戏归约，并给出修改版倒计时游戏的自包含 EXPSPACE 完全性证明：初始计数器值由第一玩家自由选择而非给定。文章还给出上界的替代证明，简化 belt theorem，得到非 succinct 情形的多项式空间算法，并可扩展到 succinct 情形的指数空间算法。
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).
@article{paperbot2239,
title = {Countdown games, and simulation on (succinct) one-counter nets},
author = {Petr Jancar and Petr Osicka and Zdenek Sawa},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 1},
year = {2023},
doi = {10.46298/lmcs-19(1:11)2023}
}