随机计时博弈再探

由 Bouyer 和 Forejt 引入的随机计时博弈（STG）自然地推广了连续时间马尔可夫链和时间自动机，它通过将位置划分为由具有竞争目标的两位玩家（玩家 Box 和玩家 Diamond）控制的部分以及由随机规律控制的部分。根据玩家数量——$2$、$1$ 或 $0$——随机计时博弈的子类通常被分类为 $2\frac{1}{2}$-玩家、$1\frac{1}{2}$-玩家和 $\frac{1}{2}$-玩家博弈，其中 $\frac{1}{2}$ 象征着随机“自然”玩家的存在。对于具有可达性目标的 STG，已知 $1\frac{1}{2}$-玩家单时钟 STG 对于定性目标是可判定的，而 $2\frac{1}{2}$-玩家三时钟 STG 对于定量可达性目标是不可判定的。本文进一步细化了这一可判定性谱系中的空白。我们证明，定量可达性目标对于 $1\frac{1}{2}$ 玩家四时钟 STG 已经是不可判定的，甚至在时间有界限制下对于 $2\frac{1}{2}$-玩家五时钟 STG 也是不可判定的。我们还获得了一类 $1\frac{1}{2}$、$2\frac{1}{2}$ 玩家 STG，其定量可达性问题是可判定的。