## Department of Computer Sciences## 1999 ACL2 WorkshopMarch 29 - March 31, 1999 |

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

Last updated March 1999 pete@cs.utexas.edu |
Computer Sciences
Department University of Texas at Austin |