Graded Alternating-Time Temporal Logic
- 610 Downloads
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.
KeywordsDecision Point Outgoing Edge Winning Strategy Atomic Proposition Computation Tree Logic
Unable to display preview. Download preview PDF.
- 1.Ågotnes, T., Goranko, V., Jamroga, W.: Alternating-time temporal logics with irrevocable strategies. In: Proc. of TARK 2007, pp. 15–24. ACM, New York (2007)Google Scholar
- 4.Bianco, A., Mogavero, F., Murano, A.: Graded computation tree logic. In: Proc. of LICS 2009 (2009)Google Scholar
- 6.Ferrante, A., Memoli, M., Napoli, M., Parente, M., Sorrentino, F.: A NuSMV extension for graded-CTL model checking. In: Proc. of CAV 2010 (2010)Google Scholar
- 7.Ferrante, A., Murano, A., Parente, M.: Enriched μ-calculi module checking. Logical Methods in Computer Science 4(3) (2008)Google Scholar
- 12.Gradel, E., Otto, M., Rosen, E.: Two-variable logic with counting is decidable. In: Proc. of LICS 1997 (1997)Google Scholar
- 13.Hollunder, B., Baader, F.: Qualifying number restrictions in concept languages. In: 2nd International Conference on Principles of Knowledge Representation and Reasoning, pp. 335–346 (1991)Google Scholar