Local Model Checking in the Modal Mu-Calculus
C. Stirling and D. WalkerAbstract: 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.
Previous | Index | Next