@inproceedings{c53b28f8f12948739b595040b7f69669,

title = "Solving disjunctive/conjunctive boolean equation systems with alternating fixed points",

abstract = "This paper presents a technique for the resolution of alternating disjunctive/conjunctive boolean equation systems. The technique can be used to solve various verification problems on finite-state concurrent systems, by encoding the problems as boolean equation systems and determining their local solutions. The main contribution of this paper is that a recent resolution technique from [13] for disjunctive/conjunctive boolean equation systems is extended to the more general disjunctive/conjunctive forms with alternation. Our technique has the time complexity O(m+n 2), where m is the number of alternation free variables occurring in the equation system and n the number of alternating variables. We found that many µ-calculus formulas with alternating fixed points occurring in the literature can be encoded as boolean equation systems of disjunctive/conjunctive forms. Practical experiments show that we can verify alternating formulas on state spaces that are orders of magnitudes larger than reported up till now.",

author = "J.F. Groote and M.K. Kein{\"a}nen",

year = "2004",

doi = "10.1007/978-3-540-24730-2_33",

language = "English",

isbn = "3-540021299-X",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "436--450",

editor = "K. Jensen and A. Podelski",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems (Proceedings TACAS 2004, Part of ETAPS 2004, Barcelona, Spain, March 29-April 2, 2004)",

address = "Germany",

}