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

This paper introduces Graded Computation Tree Logic with finite path semantics (GCTLf ⁎, 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 GCTLf ⁎ are interpreted over Kripke structures. The syntax of GCTLf ⁎ has path quantifiers of the form E≥gψ which express that there are at least g many distinct finite paths that satisfy ψ. After defining and justifying the logic GCTLf ⁎, we solve its model checking problem and establish that its computational complexity is PSPACE-complete. Moreover, we investigate GCTLf ⁎ under the imperfect information setting. Precisely, we introduce GCTLKf ⁎, an epistemic extension of GCTLf ⁎ and prove that the model checking problem also in this case is PSPACE-complete. © 2019 Elsevier B.V.