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).

翻译：我们回答了Hofman、Lasota、Mayr、Totzke（LMCS 2016）关于简洁单计数器网（即无零测试的单计数器自动机，其计数器增减量为二进制整数）上模拟预序的一个开放复杂度问题；该问题已知为PSPACE-hard且属于EXPSPACE。我们证明，对于这些网，双模拟等价与模拟预序之间的所有关系均为EXPSPACE-hard；因此模拟预序是EXPSPACE完全的。该结果通过归约到可达性博弈得到证明，而Hunter（RP 2015）利用其他结果已证明简洁单计数器网情况下可达性博弈的EXPSPACE完全性。我们还为此类可达性博弈的一个特例（即Jurdzinski、Sproston、Laroussinie（LMCS 2008）证明为EXPTIME完全的倒计时博弈的修改版）提供了直接且自包含的EXPSPACE完全性证明；在我们的修改版中，初始计数器值并非给定，而是由第一个玩家自由选择。此外，我们提出了Hofman等人上界的另一种证明。特别地，我们给出了带定理的一个新简化证明，该证明为（非简洁）单计数器网上的模拟预序提供了简单的图形表示，并导出了一个多项式空间算法（该算法可轻易扩展为简洁单计数器网的指数空间算法）。