Nicolas Markey

Abstract

We investigate the path model checking problem for the μ-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 μ-calculus.

@article{ipl97(6)-MS,
  author =              {Markey, Nicolas and Schnoebelen, {\relax Ph}ilippe},
  title =               {Mu-calculus path checking},
  publisher =           {Elsevier},
  journal =             {Information Processing Letters},
  volume =              {97},
  number =              {6},
  pages =               {225-230},
  year =                {2006},
  month =               mar,
  doi =                 {10.1016/j.ipl.2005.11.010},
  abstract =            {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.},
}