Academic
Publications
The Complexity of CTL* + Linear Past

The Complexity of CTL* + Linear Past,10.1007/978-3-540-78499-9_14,Laura Bozzelli

The Complexity of CTL* + Linear Past   (Citations: 2)
BibTex | RIS | RefWorks Download
We investigate the complexity of satisfiability and finite-state model-checking problems for the branching-time logic CTL *lp^*_{lp} , an extension of CTL* with past-time operators, where past is linear, finite, and cumulative. It is well-known that CTL *lp^*_{lp} has the same expressiveness as standard CTL*, but the translation of CTL *lp^*_{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^*_{lp} is 2Exptime-complete, which is the same complexity as that of CTL*, but for the existential fragment of CTL *lp^*_{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^*_{lp} . For full CTL *lp^*_{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^*_{lp} remains open: it lies somewhere between Expspace and 2Exptime.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...A two-way version of these automata was studied by Bozzelli (2008)...

    Volker Weber. Branching-Time Logics Repeatedly Referring to States

    • ...In both cases, past modalities do not increase the complexity: PCTL is EXPTIME-complete [16] and PCTL ∗ has recently been shown to be 2EXPTIME-complete by Bozzelli [3]...
    • ...They allow for an easy translation from CTL ∗ [18] and have proved useful in studies of CTL ∗ with past [17,3]...
    • ...Symmetric two-way HAA have been used by Bozzelli to prove membership in 2EXPTIME for CTL ∗ with past [3]...
    • ...do not enforce that infinite paths in a run move only downward in the tree from a certain point on. Therefore, our results on symmetric two-way HAA are not implied by [3]...
    • ...Nevertheless, the restricted version of [3] would suffice to prove our results on the complexity of branching-time logics...
    • ...This yields the following theorem, which has been proved before by Bozzelli for a slightly more restricted model [3]...

    Volker Weber. On the Complexity of Branching-Time Logics

Sort by: