QCTL model-checking with QBF solvers

TL;DR

This paper introduces a new approach for model-checking Quantified CTL (QCTL) by reducing the problem to QBF, enabling the use of QBF solvers to verify complex properties over Kripke structures.

Contribution

It presents a novel reduction-based algorithm for QCTL model-checking and compares different strategies using various QBF solvers.

Findings

Reduction strategies vary in efficiency

QBF solvers can effectively handle QCTL model-checking

Prototype implementation demonstrates practical viability

Abstract

Quantified CTL (QCTL) extends the temporal logic CTL with quantifications over atomic propositions. This extension is known to be very expressive: QCTL allows us to express complex properties over Kripke structures (it is as expressive as MSO). Several semantics exist for the quantifications: here, we work with the structure semantics, where the extra propositions label the Kripke structure (and not its execution tree), and the model-checking problem is known to be PSPACE-complete in this framework. We propose a new model-checking algorithm for QCTL based on a reduction to QBF. We consider several reduction strategies and we compare them with a prototype (based on several QBF solvers) on different examples.