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]. The two approaches are described very differently and are based on different principles. k-LIVENESS works by translating the liveness property together with fairness constraints to the form FGq, and then bounding the number of times 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. In this paper, we present an algorithm k-FAIR that builds on top of the ideas of k-LIVENESS and FAIR, and that suitably combines the strengths of both approaches. The experiments on the hardware model checking and industrial benchmarks show the promise of the new approach.

References: [1] K. Claessen and N. Sorensson, "A liveness checking algorithm that counts," FMCAD 2012. [2] A. Bradley, F. Somenzi, Z. Hassan, and Y. Zhang, "An incremental approach to model checking progress properties," FMCAD 2011.