Aminof, B., Murano, A., & Rubin, S. (2015). On CTL∗ with Graded Path Modalities. In Logic for Programming, Artificial Intelligence, and Reasoning. 20th International Conference, LPAR-20 2015 ; Davis, Martin; Fehnker, Ansgar; McIver, Annabelle; Voronkov, Andrei. Fiji Islands. https://doi.org/10.1007/978-3-662-48899-7_20
Graded path modalities count the number of paths satisfying a property, and generalize the existential (E) and universal (A) path modalities of CTL∗. The resulting logic is denoted GCTL∗, and is a very powerful logic since (as we show) it is equivalent, over trees, to monadic path logic. We settle the complexity of the satisfiability problem of GCTL∗, i.e., 2ExpTime-Complete, and the complexity of the model checking problem of GCTL∗, i.e., PSpace-Complete. The lower bounds already hold for CTL∗, and so we supply the upper bounds. The significance of this work is two-fold: GCTL∗ is much more expressive than CTL∗ as it adds to it a form of quantitative reasoning, and this is done at no extra cost in computational complexity.
en
Additional information:
The final publication is available via <a href="https://doi.org/10.1007/978-3-662-48899-7_20" target="_blank">https://doi.org/10.1007/978-3-662-48899-7_20</a>.