Quirky Quantifiers: Optimal Models and Complexity of Computation Tree Logic
Logic in Computer Science
2017-02-27 v3 Computational Complexity
Abstract
The satisfiability problem of the branching time logic CTL is studied in terms of computational complexity. Tight upper and lower bounds are provided for each temporal operator fragment. In parallel, the minimal model size is studied with a suitable notion of minimality. Thirdly, flat CTL is investigated, i.e., formulas with very low temporal operator nesting depth. A sharp dichotomy is shown in terms of complexity and minimal models: Temporal depth one has low expressive power, while temporal depth two is equivalent to full CTL.
Cite
@article{arxiv.1510.08786,
title = {Quirky Quantifiers: Optimal Models and Complexity of Computation Tree Logic},
author = {Martin Lück},
journal= {arXiv preprint arXiv:1510.08786},
year = {2017}
}