On How Bit-Vector Logic Can Help Verify LTL-Based Specifications

This paper studies how bit-vector logic (bv logic) can help improve the efficiency of verifying specifications expressed in Linear Temporal Logic (LTL). First, it exploits the notion of Bounded Satisfiability Checking to propose an improved encoding of LTL formulae into formulae of bv logic, which can be formally verified by means of Satisfiability Modulo Theories (SMT) solvers. To assess the gain in efficiency, we compare the proposed encoding, implemented in our tool $\mathbb {Z}$ot, against three well-known encodings available in the literature: the classic bounded encoding and the optimized, incremental one, as implemented in both NuSMV and nuXmv, and the encoding optimized for metric temporal logic, which was the “standard” implementation provided by $\mathbb {Z}$ot. We also compared the newly proposed solution against five additional efficient algorithms proposed by nuXmv, which is the state-of-the-art tool for verifying LTL specifications. The experiments show that the new encoding provides significant benefits with respect to existing tools. Since the first set of experiments only used Z3 as SMT solver, we also wanted to assess whether the benefits were induced by the specific solver or were more general. This is why we also embedded different SMT solvers in $\mathbb {Z}$ot. Besides Z3, we also carried out experiments with CVC4, Mathsat, Yices2, and Boolector, and compared the results against the first and second best solutions provided by either NuSMV or nuXmv. Obtained results witness that the benefits of the bv logic encoding are independent of the specific solver. Bv logic-based solutions are better than traditional ones with only a few exceptions. It is also true that there is no particular SMT solver that outperformed the others. Boolector is often the best as for memory usage, while Yices2 and Z3 are often the fastest ones.

1 Introduction

Linear Temporal Logic [1] (LTL) plays a key role in computer science. It has been used for the specification and verification of (possibly safety-critical) programs [2], the generation of test cases [3], the synthesis of controllers [4], the formalization of notations (e.g., UML) [5], the run-time verification of systems [6], and as planning formalism [7]. However, one of the key factors that still hamper the widespread adoption of this formalism in practice is the limited efficiency and scalability of verification tools.