A Graphical u-Calculus and Local Model Checking

A graphical notation for the propositional u-calculus, called modal graphs, is presented. It is shown that both the textual andequational presentations of the u-calculus can be translated intomodal graphs. A model checking algorithm based on such graphs isproposed. The algorithm is truly local in the sense that it onlygenerates the parts of the underlying search space which are necessaryfor the computation of the final result. The correctness of thealgorithm is proven and its complexity analysed.