Model checking is a formal method for verifying finite state systems properties. μ-calculus is a very expressive fix point logic capable of specifying a wide range of properties of finite state, reactive and concurrent systems. In this paper, we present a new model checking algorithm for linear and a fragment of indexed modal μ -calculus. This algorithm is based on the method of characterization of fixed point temporal logics formulae using automata. We use first recurrence automata for this purpose. Our algorithm is linear time on the size of the system model. The main contributions of this work are the efficiency of the algorithm and the first use of first recurrence automata for μ - calculus model checking.
Izadi,M. and Movaghar rahimabadi,A. (2005). An Efficient Model Checking Algorithm for a Fragment of μ-Calculus. (e215972). The CSI Journal on Computer Science and Engineering, 3(3), e215972
MLA
Izadi,M. , and Movaghar rahimabadi,A. . "An Efficient Model Checking Algorithm for a Fragment of μ-Calculus" .e215972 , The CSI Journal on Computer Science and Engineering, 3, 3, 2005, e215972.
HARVARD
Izadi M., Movaghar rahimabadi A. (2005). 'An Efficient Model Checking Algorithm for a Fragment of μ-Calculus', The CSI Journal on Computer Science and Engineering, 3(3), e215972.
CHICAGO
M. Izadi and A. Movaghar rahimabadi, "An Efficient Model Checking Algorithm for a Fragment of μ-Calculus," The CSI Journal on Computer Science and Engineering, 3 3 (2005): e215972,
VANCOUVER
Izadi M., Movaghar rahimabadi A. An Efficient Model Checking Algorithm for a Fragment of μ-Calculus. CSIonJCSE, 2005; 3(3): e215972.
The CSI Journal on Computer Science and Engineering