arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2008.11753cs.LO
收藏

倒计时博弈,以及(简洁)单计数器网上的模拟

Countdown games, and simulation on (succinct) one-counter nets

Petr Jancar, Petr Osicka, Zdenek Sawa

AI总结:

该文证明简洁单计数器网上的模拟预序为EXPSPACE完全,通过归约可达性博弈并给出倒计时博弈变体的直接证明,同时简化了带定理以提供新的上界证明。

摘要:

我们回答了Hofman、Lasota、Mayr和Totzke(LMCS 2016)关于简洁单计数器网(即无零测试的单计数器自动机,其中计数器增减量以二进制整数表示)上模拟预序的一个开放复杂度问题;该问题已知为PSPACE困难且属于EXPSPACE。我们证明,对于这些网,双模拟等价与模拟预序之间的所有关系都是EXPSPACE困难的;因此模拟预序是EXPSPACE完全的。该结果通过从可达性博弈归约得到,而Hunter(RP 2015)已证明简洁单计数器网情形下可达性博弈的EXPSPACE完全性,并利用了其他结果。我们还为这类可达性博弈的一个特例提供了直接且自包含的EXPSPACE完全性证明,即对Jurdzinski、Sproston和Laroussinie(LMCS 2008)证明为EXPTIME完全的倒计时博弈的一种修改;在我们的修改中,初始计数器值并非给定,而是由第一位玩家自由选择。我们还给出了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).

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑