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 ψ which express that there are at least g many distinct finite paths that satisfy ψ. 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.

Authors

• Aniello Murano University of Naples Federico II
• Mimmo Parente
• Sasha Rubin
• Loredana Sorrentino

Keywords

• Computation tree logic
• Model checking
• Finite paths