# Pushdown System

A *pushdown* *system* is a triple $\mathcal{P}=(P,\mathrm{\Gamma},\mathrm{\Delta})$ where $P$ and $\mathrm{\Gamma}$ are finite sets called the *control* *locations* and the *stack* *alphabet*, respectively. A *configuration* is a pair $\ll p,w\gg $, such that $p\in \mathcal{P}$ and $w\in {\mathrm{\Gamma}}^{\ast}$, i.e., a control location with a sequence of stack elements. The finite set $\mathrm{\Delta}$ is composed of *rules*. A rule has the form $\ll p,\gamma \gg \to \ll {p}^{\prime},w\gg $, where $p,{p}^{\prime}\in \mathcal{P}$, $\gamma \in \mathrm{\Gamma}$, and $w\in {\mathrm{\Gamma}}^{\ast}$.

[0] Späth, Johannes, Karim Ali, and Eric Bodden. “Context-, flow-, and field-sensitive data-flow analysis using synchronized Pushdown systems.” Proceedings of the ACM on Programming Languages 3.POPL (2019): 48.