CTL* with graded path modalities

Graded path modalities count the number of paths satisfying a property, and generalize the existential (E) and universal (A) path modalities of . The resulting logic is denoted G, and is a powerful logic since (as we show) it is equivalent, over trees, to monadic path logic. We establish the complexity of the satisfiability problem of G, i.e., 2ExpTime-Complete, the complexity of the model checking problem of G, i.e., PSpace-Complete, and the complexity of the realizability/synthesis problem of G, i.e., 2ExpTime-Complete. The lower bounds already hold for , and so we supply the upper bounds. The significance of this work is that G is much more expressive than as it adds to it a form of quantitative reasoning, and this is done at no extra cost in computational complexity.