k-FAIR = k-LIVENESS + FAIR Revisiting SAT-based Liveness Algorithms

We revisit the two main SAT-based algorithms for checking liveness properties of finite-state transition systems: the k-LIVENESS algorithm of [1] and the FAIR algorithm of [2]. These approaches are fundamentally different. k-LIVENESS works by translating the liveness property together with fairness constraints to the form F Gq, and then bounding the number of times the variable q can evaluate to false. FAIR works by finding an over-approximation R of reachable states, so that no state in R is contained on a fair cycle. Each technique has unique strengths on different problems. In this paper, we present a new algorithm k-FAIR that builds upon both techniques, synergistically leveraging their strengths. Experiments demonstrate that this combined approach is stronger than running both in parallel.