# Local model checking in Park's my--calculus

Kick, Alexander

##### Abstract:

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.

 Zugehörige Institution(en) am KIT Fakultät für Informatik – Informatik für Ingenieure und Naturwissenschaftler (Inf. für Ing. u. Naturwiss.) Publikationstyp Buch Publikationsjahr 1995 Sprache Englisch Identifikator urn:nbn:de:swb:90-AAA722950 KITopen-ID: 72295 Erscheinungsvermerk Karlsruhe 1995. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1995,51.)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page