Model Checking and the Mu-calculus

There is a growing recognition of the need to apply formal mathematical methods in the design of \high con dence" computing systems. Such systems operate in safety critical contexts (e.g., air trafc control systems) or where errors could have major adverse economic consequences (e.g., banking networks). The problem is especially acute in the design of many reactive systems which must exhibit correct ongoing behavior, yet are not amenable to thorough testing due to their inherently nondeterministic nature. One useful approach for specifying and reasoning about correctness of such systems is temporal logic model checking,which can provide an e cient and expressive tool for automatic veri cation that a nite state system meets a correctness speci cation formulated in temporal logic. We describe model checking algorithms and discuss their application. To do this, we focus attention on a particularly important type of temporal logic known as the Mu-calculus.

• Type: Conference
• Year: 1996
• Where: DIMACS
• Authors: E. Allen Emerson
• Keywords: Correctness Speci Cation, DIMACS 1996, DIMACS 2001, Temporal Logic, Temporal Logic Model