About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Publication
Theoretical Computer Science
Paper
On model checking for the μ-calculus and its fragments
Abstract
In this paper, we consider the model checking problem for the μ-calculus and show that it is succinctly equivalent to the non-emptiness problem of finite-state automata on infinite binary trees with the parity acceptance condition. We also present efficient model checking algorithms for two rich subclasses of the μ-calculus formulas and relate their expressive power to well-known extensions of branching time temporal logics. © 2001 Elsevier Science B.V. All rights reserved.