Pushdown automata

A pushdown automata (PDA) is a tuple $(\mathcal{X},\mathcal{Q},\Gamma ,q_i,F,\delta )$ where:

• $\mathcal{X}$ is an alphabet (finite set of atomic symbols)
• $\mathcal{Q}=\{q_0,q_1,\dots ,q_n\}$ is a finite set of states
• $\Gamma$ is the set of symbols that can be stored on stack
• $q_i\in \mathcal{Q}$ is the initial state
• $F\subseteq \mathcal{Q}$ is the set of accepting states
• $\delta :\mathcal{Q}\times (\mathcal{X}\times ϵ)\times (\Gamma \cup ϵ)\to \mathcal{P}((\mathcal{Q}\times (\Gamma \cup ϵ)))$ is the transition function

The transition function $\delta$ maps $(state,letter,symbol)$ to a set of pairs of the form $(state,symbol)$.

• Symbol in domain is to be popped.
• Symbol in co-domain is to be pushed.
• If symbol is $ϵ$ (empty), nothing is to be popped / pushed.

Transitions may also be labelled $ϵ$. A word is accepted if there is any trace from initial state to accepting state that leaves the stack empty.