Local model checking for context-free processes
Hardi Hungar, Bernhard Steffen · Nordic journal of computing · 1994
We present a local model checking algorithm that decides for a given context-free process whether it satisfies a property written in the alternation-free modal mu-calculus. Heart of this algorithm is a purely syntactical sound and complete formal system, which in contrast to the known tableaux techniques, uses intermediate second-order assertions. These assertions provide a finite representation of all the infinite state sets which may arise during the proof in terms of the finite representation of the context-free argument process. This is the key to the effectiveness of our local model checking procedure.