Pushdown System

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