Department of Computer Sciences 1999 ACL2 Workshop March 29 - March 31, 1999

Mu-Calculus Model-Checking in ACL2

Automatic verification methods, in particular model-checking, have received a lot of academic interest and have enjoyed wide industrial acceptance. Given a finite-state system and a temporal logic formula, model-checking algorithms are used to decide if the system satisfies the formula. CTL, LTL, and CTL* are examples of temporal logics. All of these logics can be translated into the mu-calculus. We will present Kripke structures and the syntax and semantics of the mu-calculus formally, in ACL2. The talk will be self contained.

Panagiotis (Pete) Manolios