Paper Info
Title
A sub-quadratic algorithm for conjunctive and disjunctive boolean equation systems
Abstract
We present a new algorithm for conjunctive and disjunctive boolean equation systems which arise frequently in the verification and analysis of finite state concurrent systems. In contrast to the previously known O(e2) time algorithms, our algorithm computes the solution to such a fixpoint equation system with size e and alternation depth d in O(e log d) time (here d e). We show the correctness and complexity of the algorithm. We discuss heuristics and describe how the algorithm can be efficiently implemented. The algorithm is compared to a previous solution via experiments on verification examples. Our measurements indicate that the new algorithm makes the verification of a large class of fixpoint expressions more tractable.
Year
DOI
Venue
2005
10.1007/11560647_35
ICTAC
Keywords
Field
DocType
previous solution,alternation depth,size e,concurrent system,fixpoint expression,disjunctive boolean equation system,sub-quadratic algorithm,verification example,time algorithm,new algorithm,fixpoint equation system
Discrete mathematics,Expression (mathematics),Computer science,Correctness,Algorithm,Quadratic equation,Finite-state machine,Heuristics,Boolean algebra,Fixed point,Cornacchia's algorithm
Conference
Volume
ISSN
ISBN
3722
0302-9743
3-540-29107-5
Citations 
PageRank 
References 
4
0.59
9
Authors
2
Name
Order
Citations
PageRank
Jan Friso Groote11626154.19
Misa Keinänen2383.59