Home | Quick Search | Advanced Search | Bibliography submission | Bibliography submission using bibtex | Bibliography submission using bibtex file | Links | Help | Internal


TitleModel checking in the modal -calculus and generic solutions
Author(s) Kyriakos Kalorkoti
TypeArticle in Journal
AbstractWe 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 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 Gröbner bases is not inherent to this application, other methods of deciding the existence of roots and of elimination can also be used.
KeywordsAlgorithms, Concurrency, Programming calculi, Gröbner bases
URL http://www.sciencedirect.com/science/article/pii/S074771711000177X
JournalJournal of Symbolic Computation
Pages584 - 594
NoteGroebner Bases and Applications
Translation No
Refereed No