Sciweavers

DIMACS
1996

Model Checking and the Mu-calculus

14 years 14 days ago
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.
E. Allen Emerson
Added 02 Nov 2010
Updated 02 Nov 2010
Type Conference
Year 1996
Where DIMACS
Authors E. Allen Emerson
Comments (0)