Quantified CTL: Expressiveness and Complexity

TL;DR

This paper investigates the expressiveness and computational complexity of Quantified CTL (QCTL), an extension of CTL with propositional quantification, analyzing two semantics and establishing its equivalence to Monadic Second-Order Logic.

Contribution

It provides a comprehensive study of QCTL's expressiveness and complexity, including its equivalence to MSO and the hierarchy classifications under different semantics.

Findings

QCTL coincides with Monadic Second-Order Logic under both semantics.

Model-checking complexity varies with the number of quantifiers, populating the polynomial and exponential hierarchies.

The structure semantics leads to polynomial hierarchy complexity, while the tree semantics leads to exponential hierarchy complexity.

Abstract

While it was defined long ago, the extension of CTL with quantification over atomic propositions has never been studied extensively. Considering two different semantics (depending whether propositional quantification refers to the Kripke structure or to its unwinding tree), we study its expressiveness (showing in particular that QCTL coincides with Monadic Second-Order Logic for both semantics) and characterise the complexity of its model-checking and satisfiability problems, depending on the number of nested propositional quantifiers (showing that the structure semantics populates the polynomial hierarchy while the tree semantics populates the exponential hierarchy).