Pushdown automaton

Definition

A pushdown automaton is a tuple $M = (Q, \Sigma, \Gamma, \delta, q_0, Z_0, F)$ where:

1. $Q$ is a finite set of states;
2. $\Sigma$ is a finite input alphabet;
3. $\Gamma$ is a finite stack alphabet;
4. $\delta$ is a function from $Q \times (\Sigma \cup \set{\varepsilon}) \times \Gamma$ to the finite subsets of $Q \times \Gamma^*$, the transition function;
5. $q_0 \in Q$ is the start state and $Z_0 \in \Gamma$ is the initial stack symbol;
6. $F \subseteq Q$ is the set of accepting states.

A configuration is a triple $(q, w, \gamma)$ with $q \in Q$, $w \in \Sigma^*$ the unread input and $\gamma \in \Gamma^*$ the stack, top symbol first. For $x \in \Sigma \cup \set{\varepsilon}$, $X \in \Gamma$ and $(p, \beta) \in \delta(q, x, X)$, there is a move $(q, xw, X\gamma) \vdash (p, w, \beta\gamma)$. Let $\vdash^*$ be the reflexive and transitive closure of $\vdash$. The language accepted by $M$ is $$L(M) = \set{w \in \Sigma^* : (q_0, w, Z_0) \vdash^* (q, \varepsilon, \gamma) \text{ for some } q \in F, \ \gamma \in \Gamma^*}.$$