On the Complexity of Branching-Time Logics

TL;DR

This paper classifies the computational complexity of satisfiability problems for various extensions of branching-time logics like CTL and UB, revealing a dichotomy between 2-EXPTIME and EXPTIME complexities using novel automata techniques.

Contribution

It provides a complete complexity classification for extended branching-time logics, including a surprising 2-EXPTIME completeness result for UB with forgettable past.

Findings

Satisfiability for CTL with extensions remains in 2-EXPTIME.

A dichotomy between 2-EXPTIME and EXPTIME complexities is established.

New pebble automata are introduced for upper bound proofs.

Abstract

We classify the complexity of the satisfiability problem for extensions of CTL and UB. The extensions we consider are Boolean combinations of path formulas, fairness properties, past modalities, and forgettable past. Our main result shows that satisfiability for CTL with all these extensions is still in 2-EXPTIME, which strongly contrasts with the nonelementary complexity of CTL* with forgettable past. We give a complete classification of combinations of these extensions, yielding a dichotomy between extensions with 2-EXPTIME-complete and those with EXPTIME-complete complexity. In particular, we show that satisfiability for the extension of UB with forgettable past is complete for 2-EXPTIME, contradicting a claim for a stronger logic in the literature. The upper bounds are established with the help of a new kind of pebble automata.