一句话：研究历史确定性下推自动机（HD-PDA）的表达力与简洁性，证明其强于确定型 PDA 但非全部上下文无关语言。
本文研究有限字上的历史确定性下推自动机（HD-PDA），其非确定性可依据已构造运行、与剩余输入无关地消解（又称 good-for-games PDA）。作者证明 HD-PDA 比确定型 PDA 表达力更强，但不识别全部上下文无关语言，且与无歧义 CFL 正交；HD-PDA 可比 DPDA 指数级更简洁，而 PDA 可比 HD-PDA 双指数级更简洁。对可视下推自动机（VPA），判定 HD 性为 ExpTime 完全；HD-VPA 与确定型 VPA、VPA 之间也有指数级简洁性差距且下界紧。文中还比较 HD-PDA 与 good-for-games 自动机，证明二者在潜在无限分支博弈下等价，并研究 resolver：HD-PDA 总有位置 resolver，下推转换器可实现 HD-VPA 而非 HD-PDA 的 resolver，有限状态 resolver 的 HD-PDA 可确定化。
We study the expressiveness and succinctness of history-deterministic pushdown automata (HD-PDA) over finite words, that is, pushdown automata whose nondeterminism can be resolved based on the run constructed so far, but independently of the remainder of the input word. These are also known as good-for-games pushdown automata. We prove that HD-PDA recognise more languages than deterministic PDA (DPDA) but not all context-free languages (CFL). This class is orthogonal to unambiguous CFL. We further show that HD-PDA can be exponentially more succinct than DPDA, while PDA can be double-exponentially more succinct than HD-PDA. We also study HDness in visibly pushdown automata (VPA), which enjoy better closure properties than PDA, and for which we show that deciding HDness is ExpTime-complete. HD-VPA can be exponentially more succinct than deterministic VPA, while VPA can be exponentially more succinct than HD-VPA. Both of these lower bounds are tight. We then compare HD-PDA with PDA for which composition with games is well-behaved, i.e. good-for-games automata. We show that these two notions coincide, but only if we consider potentially infinitely branching games. Finally, we study the complexity of resolving nondeterminism in HD-PDA. Every HDPDA has a positional resolver, a function that resolves nondeterminism and that is only dependant on the current configuration. Pushdown transducers are sufficient to implement the resolvers of HD-VPA, but not those of HD-PDA. HD-PDA with finite-state resolvers are determinisable.
@article{paperbot2789,
title = {A Bit of Nondeterminism Makes Pushdown Automata Expressive and Succinct},
author = {Shibashis Guha and Ismaël Jecker and Karoliina Lehtinen and Martin Zimmermann},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 1},
year = {2024},
doi = {10.46298/lmcs-20(1:3)2024}
}