A BIT OF NONDETERMINISM MAKES PUSHDOWN AUTOMATA EXPRESSIVE AND SUCCINCT

We study the expressiveness and succinctness of history-deterministic push-down automata (HD-PDA) over finite words, that is, pushdown automata whose nonde-terminism 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 HD-PDA has a positional resolver, a function that resolves nondeterminism and that is only dependent 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.