The complexity of CTL*+ linear past

Abstract

We investigate the complexity of satisfiability and finite-state model-checking problems for the branching-time logic CTL , an extension of CTL*with past-time operators, where past is linear, finite, and cumulative. It is well-known that CTL has the same expressiveness as standard CTL*, but the translation of CTL into CTL*is of non-elementary complexity, and no elementary upper bounds are known for its satisfiability and finite-state model checking problems. In this paper, we provide an elegant and uniform framework to solve these problems, which non-trivially extends the standard automata-theoretic approach to CTL*model-checking. In particular, we show that the satisfiability problem for CTL is 2Exptime-complete, which is the same complexity as that of CTL*, but for the existential fragment of CTL , the problem is Expspace-complete, hence exponentially harder than that of the existential fragment of CTL*. For the model-checking, the problem is already Expspace-complete for the existential and universal fragments of CTL . For full CTL , the proposed algorithm runs in time polynomial in the size of the Kripke structure and doubly exponential in the size of the formula. Thus, the exact complexity of model-checking full CTL remains open: it lies somewhere between Expspace and 2Exptime. © 2008 Springer-Verlag Berlin Heidelberg.