Mu-Calculus Model-Checking

  • Panagiotis Manolios
Part of the Advances in Formal Methods book series (ADFM, volume 4)


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.


Boolean Function Temporal Logic Atomic Proposition Proof Obligation Full Path 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer Science+Business Media New York 2000

Authors and Affiliations

  • Panagiotis Manolios
    • 1
  1. 1.Department of Computer SciencesUniversity of Texas at AustinUSA

Personalised recommendations