The Complexity of CTL* + Linear Past

We investigate the complexity of satisfiability and finite-state model-checking problems for the branching-time logic CTL

$^*_{lp}$

, an extension of CTL* with past-time operators, where past is linear, finite, and cumulative. It is well-known that CTL

$^*_{lp}$

has the same expressiveness as standard CTL*, but the translation of CTL

$^*_{lp}$

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

$^*_{lp}$

is

2Exptime

-complete, which is the same complexity as that of CTL*, but for the existential fragment of CTL

$^*_{lp}$

, 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

$^*_{lp}$

. For full CTL

$^*_{lp}$

, 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

$^*_{lp}$

remains open: it lies somewhere between

Expspace

and

2Exptime

.