Computer-Aided Reasoning: ACL2 Case Studies, pages 93-111. Kluwer Academic Publishers, June 2000.
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)