A Graphical μ-Calculus and Local Model Checking

摘要

A graphical notation for the prepositional μ-calculus, called modal graphs, is presented. It is shown that both the textual and equational presentations of the μ-calculus can be translated into modal graphs. A model checking algorithm based on such graphs is proposed. The algorithm is truly local in the sense that it only generates the parts of the underlying search space which are necessary for the computation of the final result. The correctness of the algorithm is proven and its complexity analysed.