Graded alternating-time temporal logic

Abstract

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. 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. Both μ-calculus and Ctl naturally apply as specification languages for closed systems: in this paper, we add graded modalities to the Alternating-time Temporal Logic (Atl) introduced by Alur et al., to study how these modalities may affect specification languages for open systems. We present, and compare with each other, three different semantics. We first consider a natural interpretation which seems suitable to off-line synthesis applications and then we restrict it to the case where players can only employ memoryless strategies. Finally, we strengthen the logic by means of a different interpretation which may find application in the verification of fault-tolerant controllers. For all the interpretations, we efficiently solve the model-checking problem both in the concurrent and turn-based settings, proving its PTIME-completeness. To this aim we also exploit also a characterization of the maximum grading value of a given formula. © 2010 Springer-Verlag.