On the complexity of branching-time logics

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 2EXPTIME, 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 2EXPTIME-complete and those with EXPTIME-complete complexity. In particular, we show that satisfiability for the extension of UB with forgettable past is complete for 2EXPTIME, 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. © 2009 Springer Berlin Heidelberg.