Details:
Title  Model checking in the modal calculus and generic solutions  Author(s)  Kyriakos Kalorkoti  Type  Article in Journal  Abstract  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 Gröbner bases to determine which choices, if any, of quantifiers in a formula (and all subformulae) 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 #Pcomplete. The use of Gröbner bases is not inherent to this application, other methods of deciding the existence of roots and of elimination can also be used.  Keywords  Algorithms, Concurrency, Programming calculi, Gröbner bases  ISSN  07477171 
URL 
http://www.sciencedirect.com/science/article/pii/S074771711000177X 
Language  English  Journal  Journal of Symbolic Computation  Volume  46  Number  5  Pages  584  594  Year  2011  Note  Groebner Bases and Applications  Edition  0  Translation 
No  Refereed 
No 
