Model-checking graded computation-tree logic with finite path semantics

This paper introduces Graded Computation Tree Logic with finite path semantics (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. The syntax of GCTL(f)* has path quantifiers of the form E->= g psi which express that there are at least g many distinct finite paths that satisfy psi. After defining and justifying the logic GCTL(f)*, we solve its model checking problem and establish that its computational complexity is PSPACE-complete. Moreover, we investigate GCTL(f)* under the imperfect information setting. Precisely, we introduce GCTLK(f)*, an epistemic extension of GCTL(f)* and prove that the model checking problem also in this case is PSPACE-complete. (C) 2019 Elsevier B.V. All rights reserved.