On CTL* with Graded Path Modalities

Abstract Graded path modalities count the number of paths satisfying a property, and generalize the existential ( \(\mathsf {E}\) ) and universal \((\mathsf {A})\) path modalities of \(\textsc {CTL}^{*}\). The resulting logic is denoted \(\textsc {G}\textsc {CTL}^{*}\), 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 \(\textsc {G}\textsc {CTL}^{*}\), i. e. , 2 ExpTime - Complete, and the complexity of the model checking problem of \(\textsc {G}\textsc {CTL}^{*}\), i. e. , PSpace - Complete. The lower bounds already hold for \(\textsc {CTL}^{*}\), and so we supply the upper bounds. The significance of this work is two-fold: \(\textsc {G}\textsc {CTL}^{*}\) is much more expressive than \(\textsc {CTL}^{*}\) as it adds to it a form of quantitative reasoning, and this is done at no extra cost in computational complexity.

Authors

• Benjamin Aminof
• Aniello Murano
• Sasha Rubin

Keywords

No keywords are indexed for this paper.