LARA

Model Checking Systems with Procedures

Suppose we have a system given by a context-free grammar $G$ and a specification given by a regular language $S$.

System meets the specification iff $L(G) \subseteq L(S)$, that is

\begin{equation*}
    L(M) \cap L(S)^c = \emptyset
\end{equation*}

Note:

  • $L(S)$ is a regular language
  • $L(S)^c$ is also a regular language
  • intersection of a context-free and regular language is a context-free language (and we can compute a grammar for it)
  • it is decidable to check if a given grammar is empty

Recall how the intersection of context-free and regular language works:

  • create a pushdown automaton for the context-free language
  • create a finite state automaton for the regular language
  • apply product construction: finite control is as in intersection of regular languages, stack is as in the original pushdown automaton

Next: a direct approach that combines the above individual constructions into one