A liveness checking algorithm that counts

We present a simple but novel algorithm for checking liveness properties of finite-state systems, called k-Liveness, which is based on counting and bounding the number of times a fairness constraint can become true. Our implementation of the algorithm is completely SAT-based, works fairly well in practice, and is competitive in performance with alternative methods. In addition, we present a pre-processing technique which can automatically derive extra fairness constraints for any given liveness problem. These constraints can be used to potentially boost the performance of any liveness algorithm. The experimental results show that the extra constraints are particularly beneficial in combination with our k-Liveness algorithm.