Satisfiability and Model Checking of CTL* with Graded Path Modalities

TL;DR

This paper introduces GCTL*, an extension of CTL* with graded path modalities, establishing its satisfiability and model checking complexities, and demonstrating its increased expressiveness without added computational cost.

Contribution

It proves the 2ExpTime-Completeness of GCTL* satisfiability and PSpace-Completeness of model checking, showing enhanced expressiveness over CTL* with no extra complexity.

Findings

GCTL* is more expressive than CTL*.

Satisfiability of GCTL* is 2ExpTime-Complete.

Model checking for GCTL* is PSpace-Complete.

Abstract

Graded path modalities count the number of paths satisfying a property, and generalize the existential (E) and universal (A) path modalities of CTL*. The resulting logic is called GCTL*. We settle the complexity of satisfiability of GCTL*, i.e., 2ExpTime-Complete, and the complexity of the model checking problem for GCTL*, i.e., PSpace-Complete. The lower bounds already hold for CTL*, and so, using the automata-theoretic approach we supply the upper bounds. The significance of this work is two-fold: GCTL* is more expressive than CTL* at no extra cost in computational complexity, and GCTL* has all the advantages over GCTL (CTL with graded path modalities) that CTL* has over CTL, e.g., the ability to express fairness.