概率互模拟的博弈刻画及其在下推自动机中的应用
计算机科学中的逻辑
2023-06-22 v3 形式语言与自动机理论
摘要
我们研究概率下推自动机（pPDA）及其子类的互模拟问题。我们对 pPDA 的定义允许概率性与非确定性分支，推广了经典的下推自动机概念（无 epsilon 转移）。我们首先给出了概率互模拟基于二人博弈的一般刻画，该刻画自然地将概率标记转移系统的互模拟检查归约为标准（非确定性）标记转移系统的互模拟检查。该归约可轻易在 pPDA 框架中实现，从而可使用标准（非概率）PDA 及其子类的已知结果。直接使用该归约会导致复杂度指数级增长，但由于该问题具有非初等复杂度，这在推导 pPDA 互模拟的可判定性时无关紧要。在概率单计数器自动机（pOCA）、概率可见下推自动机（pvPDA）和概率基本进程代数（即单状态 pPDA）的情形中，我们展示了隐式使用该归约可避免复杂度增长；因此我们分别得到 PSPACE、EXPTIME 和 2-EXPTIME 的上界，如同各自的非概率版本。已知 OCA 和 vPDA 的互模拟问题具有匹配的下界（因此分别为 PSPACE 完全和 EXPTIME 完全）；我们展示了这些下界也适用于不使用非确定性的全概率版本。
引用
@article{arxiv.1711.06120,
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= {arXiv preprint arXiv:1711.06120},
year = {2023}
}