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.