Advertisement

Graded Alternating-Time Temporal Logic

  • Marco Faella
  • Margherita Napoli
  • Mimmo Parente
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6355)

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.

Keywords

Decision Point Outgoing Edge Winning Strategy Atomic Proposition Computation Tree Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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
  2. 2.
    Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49, 672–713 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: Mocha: modularity in model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 521–525. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  4. 4.
    Bianco, A., Mogavero, F., Murano, A.: Graded computation tree logic. In: Proc. of LICS 2009 (2009)Google Scholar
  5. 5.
    Brihaye, T., Da Costa Lopes, A., Laroussinie, F., Markey, N.: Atl with strategy contexts and bounded memory. In: Artemov, S., Nerode, A. (eds.) LFCS 2009. LNCS, vol. 5407, pp. 92–106. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  6. 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. 7.
    Ferrante, A., Murano, A., Parente, M.: Enriched μ-calculi module checking. Logical Methods in Computer Science 4(3) (2008)Google Scholar
  8. 8.
    Ferrante, A., Napoli, M., Parente, M.: CTL model-checking with graded quantifiers. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 18–32. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  9. 9.
    Ferrante, A., Napoli, M., Parente, M.: Graded-CTL: satisfiability and symbolic model-checking. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 306–325. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  10. 10.
    Ferrante, A., Napoli, M., Parente, M.: Model-checking for graded CTL. Fundamenta Informaticae 96(3), 323–339 (2009)MathSciNetzbMATHGoogle Scholar
  11. 11.
    Fine, K.: In so many possible worlds. Notre Dame Journal of Formal Logic 13(4), 516–520 (1972)MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Gradel, E., Otto, M., Rosen, E.: Two-variable logic with counting is decidable. In: Proc. of LICS 1997 (1997)Google Scholar
  13. 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
  14. 14.
    Immerman, N.: Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci. 22(3), 384–406 (1981)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Kupferman, O., Sattler, U., Vardi, M.Y.: The complexity of the graded μ-calculus. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, p. 423. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  16. 16.
    Lawler, E.L.: A procedure for computing the k best solutions to discrete optimization problems and its application to the shortest path problem. Management Science 18(7), 401–405 (1972)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Lomuscio, A., Raimondi, F.: Mcmas: A model checker for multi-agent systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 450–454. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  18. 18.
    Martin, D.A.: Borel determinacy. Annals of Mathematics 102(2), 363–371 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Thomas, W.: On the synthesis of strategies in infinite games. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 1–13. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  20. 20.
    van der Hoek, W., Wooldridge, M.: Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications. Studia Logica 75(1), 125–157 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Yen, J.Y.: Finding the k shortest loopless paths in a network. Management Science 17(11), 712–716 (1971)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Marco Faella
    • 1
  • Margherita Napoli
    • 2
  • Mimmo Parente
    • 2
  1. 1.Università di Napoli “Federico II”NapoliItaly
  2. 2.Università di SalernoFiscianoItaly

Personalised recommendations