Pre*: The Predecessors of a Regular Language w.r.t. a Context-Free Grammar, with Applications

Let $L$ be a language, $G$ a context-free grammar and let $pre^*(L)$ be the language of all predecessors (w.r.t. $G$) of words in $L$. The following fact has been rediscovered in the literature repeatedly: If $L$ is regular, so is $pre^*(L)$. Moreover, given an NFA $M$ for $L$, an NFA $M'$ for $pre^*(L)$ can be computed very elegantly from $M$. Starting from a suitable $M$, simple checks on $M'$ provide solutions to many elementary decision problems concerning $G$, such as the word-problem, emptiness problem, and more. We formalize two algorithms to compute $pre^*(L)$ for a regular $L$ (using NFAs as representation). The first one is very simple and elegant and works for any CFG, while the second one is more efficient but is restricted to CFGs in in extended-CNF. All our algorithms are executable, allowing many basic problems on context-free grammars to be solved automatically.