## Local Model Checking in the Modal Mu-Calculus

**C. Stirling and D. Walker**
*Abstract:* A local model checker for the modal mu-calculus
is presented as a tableau system together with proof of its
soundness, completeness and decidability. The model checker is
*local* in the sense that it determines whether or not a
particular state *s* has a given property *A* by using
the structure of *A* and the structure of the model local to
*s*. The crux of the method is a form of fixpoint induction
refined through the use of propositional constants.

*ECS-LFCS-89-78*

Previous |

Index |

Next