关于双模拟等价判定下推过程与一阶语法的语义有限性
计算机科学中的逻辑
2019-09-25 v3 形式语言与自动机理论
摘要
证明了判定下推自动机（PDA）的给定配置是否与某个（未指定的）有限状态过程双模拟等价的问题是可想的。该可判定性是在一阶语法的框架内证明的，该框架由重写一阶项根部的有限标记规则集给出。该框架等价于允许确定性（即无选择）-步的 PDA，即 S\'enizergues 展示了复杂双模拟等价判定过程（1998, 2005）的模型。此处将此类过程用作算法的黑盒部分。该结果扩展了 Stearns (1967) 证明的确定性 PDA 正则性问题的可判定性，后来 Valiant (1975) 在复杂度方面对其进行了改进。关于非确定性 PDA 的可判定性问题（正如 Broadbent 和 G"oller, 2012 所指出的那样，此前一直是开放问题），在此得到了肯定的回答。
引用
@article{arxiv.1305.0516,
title = {Deciding semantic finiteness of pushdown processes and first-order grammars w.r.t. bisimulation equivalence},
author = {Petr Jancar},
journal= {arXiv preprint arXiv:1305.0516},
year = {2019}
}
备注
Parts of the proofs have been simplified (w.r.t. the previous version)