Affiliations: Dip.to di Informatica ed Applicazioni Universit`a di
Salerno, Italy. E-mail: {ferrante,napoli,parente}@dia.unisa.it
Abstract: Recently, complexity issues related to the decidability of the
μ-calculus, when the universal and existential quantifiers are augmented with
graded modalities, have been investigated by Kupfermann, Sattler and Vardi
([19]). Graded modalities refer to the use of the universal and existential
quantifiers with the added capability to express the concept of at least k or
all but k, for a non-negative integer k. In this paper we study the
Computational Tree Logic CTL, a branching time extension of classical modal
logic, augmented with graded modalities and investigate the complexity issues
with respect to the model-checking problem. We consider a system model
represented by a Kripke structure K and give an algorithm to solve the
model-checking problem running in time O(|K| · |φ|) which is
hence tight for the problem (here |φ| is the number of temporal and boolean
operators and does not include the values occurring in the graded modalities).
In this framework, the graded modalities express the ability to generate a
user-defined number of counterexamples to a specification φ given in CTL.
However, these multiple counterexamples can partially overlap, that is they may
share some behavior. We have hence investigated the case when all of them are
completely disjoint. In this case we prove that the model-checking problem is
both NP-hard and coNP-hard and give an algorithm for solving it running in
polynomial space. We have thus studied a fragment of graded-CTL, and have
proved that the model-checking problem is solvable in polynomial time.
Keywords: Model-checking, Computational Tree Logic, Graded Modalities
