Avoiding the Shoals - A New Approach to Liveness Checking

We present rlive, a new SAT-based model-checking algorithm for the verification of liveness properties of finite-state symbolic transition systems. Like other recent approaches, rlive works by reducing liveness checking to a sequence of safety checks. Similarly to FAIR, it incrementally strengthens the input system using constraints obtained by refuting candidate counterexamples to the input liveness property, assumed (w.l.o.g.) to be of the form FGq. Differently from FAIR (and crucially), however, instead of directly searching for lasso-shaped counterexamples visiting ¬q infinitely-often, rlive searches for counterexamples incrementally, via a recursive chain of safety checks, each of which tries to determine whether it is possible to reach a ¬q-state from a given ¬q-state (which was previously determined to be reachable), in a manner similar to k-Liveness. When the current candidate counterexample is refuted, rlive exploits the inductive invariants generated by the (recursive) safety checks to restrict the search space, until either no more reachable ¬q-states remain, or a real lasso-shaped counterexample is found. In this paper, we describe rlive in detail, prove its soundness and completeness, and compare it against the state of the art both theoretically and empirically. Our experimental results show that our implementation of rlive outperforms state-of-the-art implementations of FAIR, k-Liveness and other SAT-based liveness checking algorithms on a wide range of benchmarks from the literature.