An effective model checking for Mu-calculus: from finite systems towards systems with real time

Mu-calculus is a polymodal logic with fixed points. A Decision Procedure (DP) checks the validity of a formula. A Model-Checking Procedure (MCP) constructs the validity set of a formula in a model. Since Mu-calculus is finitely approximatizible and it is applicable for verification of Finite-State Machines an effective MCPs are of high importance. The paper deals with the direct exponential MCP and a polynomial approximation of MCP, which is correct for a representative fragment of Mu-calculus on finite models, and with an extension of a MCP for finite models to infinite models with a real time.