Mu-calculus path checking
We investigate the path model checking problem for the mu-calculus. Surprisingly, restricting to deterministic structures does not allow for more efficient model checking algorithm, as we prove that it can encode any instance of the standard model checking problem for the mu-calculus. (c) 2005 Elsevier B.V. All rights reserved.
mu-calculus model checking program correctness formal methods