一句话：用双人博弈刻画概率双相似性，并据此确定概率下推自动机及其子类的可判定性与复杂度界。
论文研究概率下推自动机（pPDA）及其子类的双相似性问题，其中 pPDA 同时允许概率与非确定分支。作者首先给出概率双相似性的双人博弈刻画，将概率标记转移系统的双相似性检查归约为标准非确定标记转移系统的双相似性检查。该归约可直接用于 pPDA，从而借助经典 PDA 的已知结果；虽导致指数级开销，但因 pPDA 本身复杂性为非初等，不影响可判定性。对概率单计数器自动机、概率可见下推自动机和概率基本进程代数，作者以隐式方式使用归约避免复杂度上升，分别得到 PSPACE、EXPTIME 和 2-EXPTIME 上界，并证明不使用非确定性的完全概率版本仍具有相应下界。
We study the bisimilarity problem for probabilistic pushdown automata (pPDA) and subclasses thereof. Our definition of pPDA allows both probabilistic and non-deterministic branching, generalising the classical notion of pushdown automata (without epsilon-transitions). We first show a general characterization of probabilistic bisimilarity in terms of two-player games, which naturally reduces checking bisimilarity of probabilistic labelled transition systems to checking bisimilarity of standard (non-deterministic) labelled transition systems. This reduction can be easily implemented in the framework of pPDA, allowing to use known results for standard (non-probabilistic) PDA and their subclasses. A direct use of the reduction incurs an exponential increase of complexity, which does not matter in deriving decidability of bisimilarity for pPDA due to the non-elementary complexity of the problem. In the cases of probabilistic one-counter automata (pOCA), of probabilistic visibly pushdown automata (pvPDA), and of probabilistic basic process algebras (i.e., single-state pPDA) we show that an implicit use of the reduction can avoid the complexity increase; we thus get PSPACE, EXPTIME, and 2-EXPTIME upper bounds, respectively, like for the respective non-probabilistic versions. The bisimilarity problems for OCA and vPDA are known to have matching lower bounds (thus being PSPACE-complete and EXPTIME-complete, respectively); we show that these lower bounds also hold for fully probabilistic versions that do not use non-determinism.
@article{paperbot357,
title = {Game Characterization of Probabilistic Bisimilarity, and Applications to Pushdown Automata},
author = {Vojtěch Forejt and Petr Jančar and Stefan Kiefer and James Worrell},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 4},
year = {2018},
doi = {10.23638/lmcs-14(4:13)2018}
}