Regular languages have robust theoretical foundations leading to numerous applications including model checking. Context-free
languages and pushdown automata have been indispensable in program analysis due to their ability to model control flow in
procedural languages, but the corresponding theory is fragile. In particular, non-closure under intersection and undecidability
of the language inclusion problem disallows context-free specifications in model checking applications.