Obtaining Memory-Efficient Solutions to Boolean Equation Systems

This paper is concerned with memory-efficient solution techniques for Boolean fixed-point equations. We show how certain structures of fixed-point equation systems, often encountered in solving verification problems, can be exploited in order to substantially improve the performance of fixed-point computations. Also, we investigate the space complexity of the problem of solving Boolean equation systems, showing a NL-hardness result. A prototype of the proposed technique has been implemented and experimental results on a series of protocol verification benchmarks are reported.