Model checking in the modal μ-calculus and generic solutions

摘要

We discuss an algebraic method for model checking in the modal μ-calculus over finite state labelled transition systems that can be used to provide solutions that are in a sense generic, i.e., in a formula the quantifiers can be left as unknowns. The resulting solution can then be used with the method of Grobner bases to determine which choices, if any, of quantifiers in a formula (and all sub-formulae) lead to chosen values for the variables. The ability to provide generic solutions can be seen as a useful tool for providing examples either for pedagogical reasons or for case studies. We show that if polynomials are represented in expanded form then in the worst case their size is exponential in the size of the input. By contrast, for the example given, the size is linear if zero suppressed binary decision diagrams are used. We also discuss counting the number of possible solutions as quantifiers are varied and show that this is #P-complete. The use of Grobner bases is not inherent to this application, other methods of deciding the existence of roots and of elimination can also be used.