Model checking for context-free processes

Abstract

We develop a model-checking algorithm that decides for a given context-free process whether it satisfies a property written in the alternationfree modal mu-calculus. The central idea behind this algorithm is to raise the standard iterative model-checking techniques to 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 property trans]ormer for each state class of the finite process representation. These property transformers can then simply be applied to solve the modelchecking 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.