= Solution
A <nondeterministic pushdown automaton> is a <tuple>
$$
M=(Q,\Sigma,\Gamma,\delta,q_0,Z_0,F),\qquad
\delta:Q\times(\Sigma\cup\{\varepsilon\})\times\Gamma
\longrightarrow\mathcal P_{\mathrm{fin}}(Q\times\Gamma^*).
$$
Here $Q$ is a nonempty <finite set> of control states, $\Sigma$ a finite input <alphabet>, $\Gamma$ a finite <stack alphabet>, $q_0\in Q$ the initial control state, $Z_0\in\Gamma$ the initial <stack> symbol, and $F\subseteq Q$ the final control states. The notation $\mathcal P_{\mathrm{fin}}$ requires each transition to have only finitely many choices. Since the domain is finite, the whole transition specification is finite.
A <pushdown automaton configuration> is $(q,w,\alpha)\in Q\times\Sigma^*\times\Gamma^*$, recording the control state, unread input <word>, and <stack> contents. Write the top of the <stack> on the left. For $a\in\Sigma$, the one-step relation is
$$
(q,aw,X\beta)\vdash_M(r,w,\gamma\beta)
\quad\text{if }(r,\gamma)\in\delta(q,a,X).
$$
An <epsilon transition> instead has
$$
(q,w,X\beta)\vdash_M(r,w,\gamma\beta)
\quad\text{if }(r,\gamma)\in\delta(q,\varepsilon,X).
$$
Thus a move replaces the top <stack> symbol $X$ by the <word> $\gamma$, whose leftmost symbol becomes the new top. It consumes one input symbol or no input symbol. Under this convention there is no move from an empty <stack>.
For <acceptance by final state>, the recognized <formal language> is
$$
\boxed{L(M)=\{w\in\Sigma^*: (q_0,w,Z_0)\vdash_M^*(f,\varepsilon,\alpha)
\text{ for some }f\in F,\ \alpha\in\Gamma^*\}.}
$$
Here $\vdash_M^*$ allows any finite number of moves, including zero. The entire input must have been consumed; the final <stack> need not be empty. Acceptance requires at least one such run of the <nondeterministic pushdown automaton>.
Back to article page
