QBF Encoding of Temporal Properties and QBF-Based Verification

ABSTRACT. SAT and QBF solving techniques have applications in various areas. SAT-solving has also been applied in the area of formal verification of temporal properties of transition system models. Because of the limited expressive succinctness, complicated verification problems cannot be naturally represented with SAT-formulas succinctly. This paper investigates QBF-applications in this area, aiming at the verification of branching-time temporal logic properties of transition system models. Branching-time temporal logic properties involve operators that may require whether there exist certain kinds of paths starting at different states of a system model. This requires the use of quantifiers in the encoding of such properties. The focus of this paper is on temporal logic properties specified by the extended computation tree logic that allows some sort of fairness, and the main contribution of this paper is a bounded semantics for the extended computation tree logic. Then a QBF encoding of the temporal logic is developed from the definition of the bounded semantics, and then an implementation of QBF-based verification follows from the QBF encoding. Experimental evaluation of the feasibility and the computational properties of such a QBF-based verification algorithm is reported.