Model Checking for Context-Free Processes
O. Burkart, B. Steffen
We develop a model-checking algorithm that decides for a given
{\em context-free} process whether it satisfies a property
written in the alternation-free modal mu-calculus. The central
idea behind this algorithm is to raise the standard iterative
model-checking techniques to {\em higher order}: in contrast
to the usual approaches, in which the set of formulas that
are satisfied by a certain state are iteratively computed, our
algorithm iteratively computes a {\em property transformer} for
each state class of the finite process representation. These
property transformers can then simply be applied to solve
the model-checking problem. The complexity of our algorithm
is linear in the size of the system's representation and
exponential in the size of the property being investigated.