# Mu-Calculus Model-Checking

Panagiotis Manolios.

Computer-Aided Reasoning: ACL2 Case Studies, pages 93-111. Kluwer Academic Publishers, June 2000.

# Abstract

Temporal logic model-checking has received substantial academic
interest and has enjoyed wide industrial acceptance. Temporal
logics are used to describe the behavior (over time) of systems
which continuously interact with their environment. Model-checking
algorithms are used to decide if a finite-state system satisfies a
temporal logic formula. Many temporal logics, *e.g.*, CTL, LTL, and
CTL* can be translated into the Mu-Calculus. In addition, the
algorithm that decides the Mu-Calculus is used for symbolic
(BDD-based) model-checking, a technique that has greatly
extended the applicability of model-checking. In this case study we
define a model-checker for the Mu-Calculus in ACL2 and show how to
translate CTL into the Mu-Calculus.

In the process of defining the Mu-Calculus, we develop (ACL2) books
on set theory, fixpoint theory, and relation theory. The development
of these books is given as a sequence of exercises. These exercises
make use of varied ACL2 features; therefore, the first few sections
may be of interest to readers who want more practice in proving
theorems in ACL2.

Gzipped Postscript (180K)