Abstract
We introduce QAPI (quantified ATL with probabilism and incomplete information), which extends epistemic and probabilistic ATL with quantification of strategies and a flexible mechanism to reason about strategies in the object language. This allows QAPI to express complex strategic properties such as equilibria and to treat the behavior of the “counter-coalition” in a very flexible way. We provide bisimulation relations, model checking results, and study the issues arising from the interplay between quantifiers and both epistemic and temporal operators.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
A probability distribution \(\mathrm {\text {Pr}}\) on \(Q\) is discrete, if there is a countable set \(Q'\subseteq Q\) such that \(\sum _{q\in Q'} \mathrm {\text {Pr}} \left( q\right) =1\).
- 2.
I.e., if \(\mathrm {S}_i\) is an \(A\)-strategy choice variable for some coalition \(A\), then \(\mathsf {S}_i\) is a strategy choice for \(A\).
- 3.
It is not sufficient to rely on the uniformity of strategy choices (the same strategy must be chosen in \(A\)-indistinguishable states), since there must be a single strategy that is successful in all \(\varGamma \)-indistinguishable states, and \(\varGamma \) might have less information than \(A\).
- 4.
To express this as a variable, the CGS needs to record the last move of each player in the state in the obvious way.
References
Ågotnes, T., Goranko, V., Jamroga, W.: Alternating-time temporal logics with irrevocable strategies. In: Samet [12], pp. 15–24
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)
Brázdil, T., Brozek, V., Forejt, V., Kucera, A.: Stochastic games with branching-time winning objectives. In: LICS, pp. 349–358. IEEE Computer Society (2006)
Chatterjee, K., Henzinger, T.A., Jurdzinski, M.: Games with secure equilibria. Theor. Comput. Sci. 365(1–2), 67–82 (2006)
Chatterjee, K., Henzinger, T.A., Piterman, N.: Strategy logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 59–73. Springer, Heidelberg (2007)
Cortier, V., Küsters, R., Warinschi, B.: A cryptographic model for branching time security properties – the case of contract signing protocols. In: Biskup, J., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 422–437. Springer, Heidelberg (2007)
Chen, T., Lu, J.: Probabilistic alternating-time temporal logic and model checking algorithm. In: Lei, J. (ed.) FSKD (2), pp. 35–39. IEEE Computer Society (2007)
Halpern, J.Y., Moses, Y.: Knowledge and common knowledge in a distributed environment. J. ACM 37, 549–587 (1990)
Herzig, A., Troquard, N.: Knowing how to play: uniform choices in logics of agency. In: Nakashima, H., Wellman, M.P., Weiss, G., Stone, P. (eds) AAMAS, pp. 209–216. ACM (2006)
Jamroga, W.: Some remarks on alternating temporal epistemic logic. In: Proceedings of Formal Approaches to Multi-Agent Systems (FAMAS 2003), pp. 133–140 (2004)
Jamroga, W., van der Hoek, W.: Agents that know how to play. Fundamenta Informaticae 63(2–3), 185–219 (2004)
Samet, D. (ed.): Proceedings of the 11th Conference on Theoretical Aspects of Rationality and Knowledge (TARK-2007), Brussels, Belgium, 25–27 June (2007)
Schobbens, P.-Y.: Alternating-time logic with imperfect recall. Electron. Notes Theoret. Comput. Sci. 85(2), 82–93 (2004)
Schnoor, H.: Strategic planning for probabilistic games with incomplete information. In: van der Hoek, W., Kaminka, G.A., Lespérance, Y., Luck, M., Sen, S. (eds) AAMAS, pp. 1057–1064. IFAAMAS (2010)
Schnoor, H.: Deciding epistemic and strategic properties of cryptographic protocols. In: Foresti, S., Yung, M., Martinelli, F. (eds.) ESORICS 2012. LNCS, vol. 7459, pp. 91–108. Springer, Heidelberg (2012)
Walther, D., van der Hoek, W., Wooldridge, M.: Alternating-time temporal logic with explicit strategies. In: Samet [12], pp. 269–278
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schnoor, H. (2014). Epistemic and Probabilistic ATL with Quantification and Explicit Strategies. In: Filipe, J., Fred, A. (eds) Agents and Artificial Intelligence. ICAART 2013. Communications in Computer and Information Science, vol 449. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44440-5_8
Download citation
DOI: https://doi.org/10.1007/978-3-662-44440-5_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44439-9
Online ISBN: 978-3-662-44440-5
eBook Packages: Computer ScienceComputer Science (R0)