A Divide and Conquer Approach to Model Checking of Liveness Properties

An approach to making liveness model checking problems under fairness feasible is described. The proposed method divides such a problem into multiple smaller ones that can be conquered such that the former is derived from the latter. Since the proposed method does not need any specialized algorithms, it can use existing LTL model checkers such as Spin, SAL and Maude LTL model checker. The proposed method also lets (or helps) humans get better understanding of the reason why they need to use fairness assumptions.