Improved complement for two-way alternating automata

The side notes in small font on the right margin of each line of pseudocode will be useful in Sect. 5, when we discuss implementation and efficiency. For now, they can be ignored.

In pseudocode, such existential branching is captured by the statement “\(\smash {\underline{\mathbf{guess }}}\) one of:,” followed by a list of •-marked code snippets: the current branch of the a fa forks into one new branch for each snippet, and accepts iff at least one of these branches accepts. When the branching is over (not multiple code snippets, but) multiple values of a variable v, then we use the statement “\(\smash {\underline{\mathbf{guess }}}\) one v”: the a fa forks into one new branch for each possible value of v, and the statement accepts iff at least one of these branches accepts. Likewise, universal branching is captured by the statements “\(\smash {\underline{\mathbf{select }}}\) one of:” and “\(\smash {\underline{\mathbf{select }}}\) one v,” which are interpreted similarly, except now the current branch accepts iff all of the new branches do. To help understand this terminology, we stress that our pseudocode is written from the perspective (not of the entire computation, but) of a single computation branch: it describes what a single branch must do when it participates (together with other branches) in the execution of a procedure. From this perspective, other usual phrases for describing existential and universal branching, like “check/verify existentially one of:” and “check/verify universally/in parallel each of:” (which are suitable from the perspective of the entire computation), are not appropriate: e.g., a single branch cannot do multiple things “in parallel,” as this requires spawning other branches; but it can certainly guess which one of many snippets is the “right” one and execute it, or select among many snippets the one “assigned” to it and execute it.

By the analysis of Sect. 5, it will be clear that l:2 in this snippet needs \(\varTheta (s^7)\) states.

Note that, in contrast, calls to procedures do not require a call stack, for two reasons: first, because the called procedure does not need to return any value; and second, because (as the reader can verify by inspection) no procedure call is ever followed by other steps in the calling procedure. Hence, the automaton can execute the called procedure independently from the calling one, i.e., without storing any information about it, as it will never need to return to it.