Local model checking in Park's my--calculus

Temporal logic model checking is an automatic verification method for
finite-state systems. In global model checking, the truth of a formula
(and its subformulae) is determined for all the states in the
model. Local model checking procedures are designed for proving that a
specific state of the model satisfies a given formula. This may avoid
the exhaustive traversal of a model. Also, the proof tree constructed
during local model checking can serve as a witness (counterexample) which
demonstrates the error in the design and can thus help locating errors.

In \cite{StiWal91} it was shown how local model checking can be
performed in the modal $\mu$-calculus. In this paper, we introduce a
tableau system and thus a local model checking method for the more
expressive $\mu$-calculus of Park \cite{Par76} and prove its soundness
and completeness.