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(e²) 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. © Springer-Verlag Berlin Heidelberg 2005.

Groote J.F., Keinanen M.

709.pdf    Gửi cho bạn bè

Từ khóa : Algorithms; Boolean algebra; Computational complexity; Heuristic methods; Conjunctive boolean equation systems; Disjunctive boolean equation systems; Fixpoint expressions; Sub-quadratic algorithms; Quadratic programming