To split or to conjoin: The question in image computation

Image computation is the key step in fixpoint computations that are extensively used in model checking. Two techniques have been used for this step: one based on conjunction of the terms of the transition relation, and the other based on recursive case splitting. We discuss when one technique outperforms the other, and consequently formulate a hybrid approach to image computation. Experimental results show that the hybrid algorithm is much more robust than the "pure" algorithms and outperforms both of them in most cases. Our findings also shed light on the remark of several researchers that splitting is especially effective in approximate reachability analysis.