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 Image 1. The resulting logic is denoted G Image 1, 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 Image 1, i. e. , 2ExpTime-Complete, the complexity of the model checking problem of G Image 1, i. e. , PSpace-Complete, and the complexity of the realizability/synthesis problem of G Image 1, i. e. , 2ExpTime-Complete. The lower bounds already hold for Image 1, and so we supply the upper bounds. The significance of this work is that G Image 1 is much more expressive than Image 1 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 University of Naples Federico II
• Sasha Rubin

Keywords

• Path quantifiers
• Graded temporal logic
• Satisfiability
• Automata theoretic approach to verification