@article {IOPORT.00751138,
    author       = {Hungar, Hardi and Steffen, Bernhard},
    title        = {Local model checking for context-free processes.},
    year         = {1994},
    journal      = {Nordic Journal of Computing},
    volume       = {1},
    number       = {3},
    issn         = {1236-6064},
    pages        = {364-385},
    publisher    = {Publishing Association Nordic Journal of Computing, Helsinki},
    abstract     = {Summary: 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. Thus is the key to the effectiveness of our local model checking procedure.},
    identifier   = {00751138},
}