# From Quantified CTL to QBF

## TL;DR

This paper introduces a model-checking algorithm for QCTL, an extension of CTL with propositional quantification, by reducing the problem to QBF and comparing different strategies using Z3.

## Contribution

It presents a novel reduction-based model-checking algorithm for QCTL, leveraging QBF solving techniques and evaluating various reduction strategies.

## Key findings

- Reduction strategies vary in efficiency
- Prototype implementation with Z3 demonstrates feasibility
- QCTL model checking is PSPACE-complete in structure semantics

## Abstract

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 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 the SMT-solver Z3) on several examples.