论文标题
倒计时游戏和（简洁的）单场网
Countdown games, and simulation on (succinct) one-counter nets
论文作者
论文摘要
我们回答了Hofman，Lasota，Mayr，Totzke（LMCS 2016）的一个开放复杂性问题，以在简洁的单场网等类别上进行模拟预订（即，一个零件自动机，没有零测试，其中计数器的增量和倒数是用二进制编写的整数）；众所周知，这个问题是pspace-hard和Expspace。我们表明，对这些网的一分化等效性和模拟预订之间的所有关系都是expace-hard。因此，模拟预订是Expass-Complete。结果是通过可达性游戏的降低来证明的，在使用其他结果的情况下，Hunter（RP 2015）显示了其在简洁的单场网中的Expspace完整性。我们还为这种可及性游戏的特殊情况提供了直接的独立空间完整性证明，即对倒计时游戏的修改，这些游戏被Jurdzinski，Sproston，Laroussinie显示出来（LMCS 2008）；在我们的修改中，没有给出初始计数器值，而是由第一个玩家自由选择。我们还为Hofman等人提供了上限的替代证明。特别是，我们给出了新简化的皮带定理证明，该证明可在（不合可能的）单场网（不合可能）预订的模拟预订中进行简单的图形表示，并导致多项式空间算法（该算法毫无用处地扩展到指数空间空间算法，以实现单相机的单相网）。
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).
