Affiliations: Department of Physics, Università di Napoli “Federico II”, Italy. mfaella@na.infn.it | Dipartimento di Informatica ed Applicazioni “R.M. Capocelli”, Università di Salerno, Italy. napoli@dia.unisa.it | Dipartimento di Informatica ed Applicazioni “R.M. Capocelli”, Università di Salerno, Italy. parente@dia.unisa.it
Note: [] Address for correspondence: Università di Napoli “Federico II”, Via Cintia, 80126 - Napoli, Italy
Abstract: Recently, temporal logics such as μ-calculus and Computational Tree Logic, CTL, augmented with graded modalities have received attention from the scientific community, both from a theoretical side and from an applicative perspective. In both these settings, graded modalities enrich the universal and existential quantifiers with the capability to express the concept of at least k or all but k, for a non-negative integer k. Both μ-calculus and CTL naturally apply as specification languages for closed systems: in this paper, we study how graded modalities may affect specification languages for open systems. We extend the Alternating-time Temporal Logic (ATL) introduced by Alur et al., that is a derivative of CTL interpreted on game structures, rather than transition systems. We solve the model-checking problem in the concurrent and turn-based settings, proving its PTIME-completeness. We present, and compare with each other, two different semantics: the first seems suitable to off-line synthesis applications while the second may find application in the verification of fault-tolerant controllers. We also study the case where players can only employ memoryless strategies, showing that also in this case the model-checking problem is in PTIME.
