Paper Info
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 M-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.
Year
DOI
Venue
2004
10.1007/978-3-540-24730-2_33
Lecture Notes in Computer Science
Keywords
Field
DocType
fixed point
Maximum satisfiability problem,Discrete mathematics,Negation normal form,Parity function,Disjunctive normal form,Boolean algebra,Fixed point,Time complexity,Boolean expression,Mathematics
Conference
Volume
ISSN
Citations 
2988
0302-9743
7
PageRank 
References 
Authors
0.54
12
2
Name
Order
Citations
PageRank
Jan Friso Groote11626154.19
Misa Keinänen2383.59