An Efficient Model Checking Algorithm for a Fragment of μ-Calculus
Abstract
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.
Keywords
model checking, verification, μ-calculus, first recurrence automata, temporal logics
