Quirky Quantifiers: Optimal Models and Complexity of Computation Tree Logic

TL;DR

This paper analyzes the computational complexity and minimal model sizes of CTL, a branching time logic, revealing a sharp dichotomy based on temporal operator nesting depth.

Contribution

It provides tight bounds for each fragment of CTL, studies minimal models, and characterizes the complexity jump at temporal depth two.

Findings

Temporal depth one has low expressive power.

Temporal depth two is as expressive as full CTL.

Precise complexity bounds are established for each fragment.

Abstract

The satisfiability problem of the branching time logic CTL is studied in terms of computational complexity. Tight upper and lower bounds are provided for each temporal operator fragment. In parallel, the minimal model size is studied with a suitable notion of minimality. Thirdly, flat CTL is investigated, i.e., formulas with very low temporal operator nesting depth. A sharp dichotomy is shown in terms of complexity and minimal models: Temporal depth one has low expressive power, while temporal depth two is equivalent to full CTL.