Graded CTL* over Finite Paths

In this paper we introduce Graded Computation Tree Logic over finite paths (GCTL∗ f, for short), a variant of Computation Tree Logic CTL∗, in which path quantifiers are interpreted over finite paths and can count the number of such paths. State formulas of GCTL∗ f are interpreted over Kripke structures with a designated set of states, which we call "check points". These special states serve to delineate the end points of the finite executions. The syntax of GCTL∗ f has path quantifiers of the form E≥gψ which express that there are at least g many distinct finite paths that a) end in a check point, and b) satisfy ψ. After defining and justifying the logic GCTL∗ f, we solve its model checking problem and establish that its computational complexity is PSPACE-complete.