Graded Alternating-Time Temporal Logic

• Autorzy: Faella M. , Napoli M. , Parente M.
• Języki publikacji: EN

Abstrakty

EN

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 applicationswhile the secondmay 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.

Słowa kluczowe

EN

turn based games; syntax; semantics; fixpoint; model checking

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 105, nr 1/2
• Strony: 189--210
• Opis fizyczny: Bibliogr. 20 poz., wykr.

Twórcy

autor

Faella M.

autor

Napoli M.

autor

Parente M.

• Universita di Napoli "Federico II", Via Cintia, 80126 - Napoli, Italy,

Bibliografia

• [1] Ågotnes, T., van der Hoek, W., Wooldridge,M.: Robust normative systems, AAMAS (2), 2008.
• [2] Ågotnes, T., van der Hoek, W., Wooldridge, M.: Robust Normative Systems and a Logic of Norm Compliance, Journal of Logic, Language and Information, 18(1), 2010, 4-30.
• [3] Ågotnes, T., Walther, D.: A Logic of Strategic Ability Under Bounded Memory, J. of Logic, Lang. and Inf., 18(1), 2009, 55-77, ISSN 0925-8531.
• [4] Alechina, N., Logan, B., Nga, N. H., Rakib, A.: A logic for coalitions with bounded resources, IJCAI'09: Proceedings of the 21st international jont conference on Artifical intelligence,Morgan Kaufmann Publishers Inc., 2009.
• [5] Alur, R., Henzinger, T., Kupferman, O.: Alternating-Time Temporal Logic, J. ACM, 49, 2002, 672-713.
• [6] Corradini, F., De Nicola, R., Labella, A.: Graded Modalities and Resource Bisimulation, Proceedings of the 19th Conference on Foundations of Software Technology and Theoretical Computer Science, Springer-Verlag, 1999, ISBN 3-540-66836-5.
• [7] Ferrante, A., Murano, A., Parente,M.: Enriched μ-Calculi Module Checking, Logical Methods in Computer Science, 4(3), 2008.
• [8] Ferrante, A., Napoli, M., Parente, M.: CTL Model-Checking with Graded Quantifiers, Proc. of ATVA '08, 5311, 2008.
• [9] Fine, K.: In so many possible worlds, Notre Dame journal of Formal Logic, 13(4), 1972, 516-520.
• [10] French, T., McCabe-Dansted, J. C., Reynolds, M.: A Temporal Logic of Robustness, LNCS 4720, FroCos, 2007.
• [11] Goranko, V., van Drimmelen, G.: Complete axiomatization and decidability of Alternating-time temporal logic, Theoretical Computer Science, 353(1-3), 2006, 93-117.
• [12] Gradel, E., Otto, M., Rosen, E.: Two-variable logic with counting is decidable, Proc. of LICS97, 1997.
• [13] Hollunder, B., Baader, F.: Qualifying Number Restrictions in Concept Languages, 2nd International Conference on Principles of Knowledge Representation and Reasoning, 1991.
• [14] Immerman, N.: Number of Quantifiers is Better Than Number of Tape Cells, J. Comput. Syst. Sci., 22(3), 1981, 384-406.
• [15] Kupferman, O., Sattler, U., Vardi, M.: The Complexity of the Graded μ-Calculus, Proc. 18th Conference on Automated Deduction, 2392, 2002.
• [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), 1972, 401-405.
• [17] Martin, D.: Borel determinacy, Annals of Mathematics, 102(2), 1975, 363-371.
• [18] Thomas, W.: On the Synthesis of Strategies in Infinite Games, Proc. of STACS95, 900, Springer-Verlag, 1995.
• [19] Walther, D., Lutz, C., Wolter, F., Wooldridge, M.: ATL Satisfiability is Indeed EXPTIME-complete, J. of Logic and Computation, 16(6), 2006.
• [20] Yen, J. Y.: Finding the K Shortest Loopless Paths in a Network, Management Science, 17(11), 1971, 712-716.