Abstract
We propose a variant of alternating time temporal logic (
) with imperfect information, perfect recall, epistemic modalities for the past and strategies which are required to be uniform with respect to distributed knowledge. The model-checking problem about 
with perfect recall and imperfect information is believed to be unsolvable, whereas in our setting it is solvable because of the uniformity of strategies. We propose a model-checking algorithm for that system, which exploits the interaction between the cooperation modalities and the epistemic modality for the past. This interaction allows every expressible goal ϕ to be treated as the epistemic goal of (eventually) establishing that ϕ holds and thus enables the handling of the cooperation modalities in a streamlined way.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Černý, P., Chaudhuri, S.: Model checking on trees with path equivalences. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 664–678. Springer, Heidelberg (2007)
Alur, R., Henzinger, T., Kupferman, O.: Alternating-time Temporal Logic. In: Proceedings of the 38th IEEE Symposium on Foundations of Computer Science, pp. 100–109 (1997)
Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM 49(5), 1–42 (2002)
Chatterjee, K., Doyen, L., Henzinger, T.A., Raskin, J.F.: Algorithms for Omega-regular Games with Imperfect Information. Logical Methods in Computer Science 3(4), 1–23 (2007)
Dix, J., Jamroga, W.: Model Checking Abilities of Agents: A Closer Look. Theory of Computing Systems 42(3), 366–410 (2008)
French, T., van der Meyden, R., Reynolds, M.: Axioms for Logics of Knowledge and Past Time: Synchrony and Unique Initial States. In: Advances in Modal Logic, vol. 5, pp. 53–72. King’s College Publications (2005)
Goranko, V., Jamroga, W.: Comparing Semantics for Logics of Multi-agent Systems. Synthese 139(2), 241–280 (2004)
Goranko, V., van Drimmelen, G.: Decidability and Complete Axiomatization of the Alternating-time Temporal Logic. Theoretical Computer Science 353(1-3), 93–117 (2006)
Halpern, J., Fagin, R., Moses, Y., Vardi, M.: Reasoning about Knowledge. MIT Press, Cambridge (1995)
Jamroga, W., Ågotnes, T.: Constructive knowledge: what agents can achieve under imperfect information. Journal of Applied Non-Classical Logics 17(4), 423–475 (2007)
Jamroga, W., van der Hoek, W.: Agents That Know How to Play. Fundamenta Informaticae 63(2-3), 185–219 (2004)
Jamroga, W., van der Hoek, W.: Strategic Ability under Uncertainty. Technical Report 6, Institute of Computer Science, Clausthal University of Technology (2006)
Kozen, D.: Results on the propositional μ-calculus. Theoretical Computer Science 27, 333–354 (1983)
Lomuscio, A., Raimondi, F.: Model checking knowledge, strategies, and games in multi-agent systems. In: Proceedings of the 5th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS 2006), pp. 161–168. ACM Press, New York (2006)
Lomuscio, A., Raimondi, F.: The Complexity of Model Checking Concurrent Programs Against CTLK Specifications. In: Baldoni, M., Endriss, U. (eds.) DALT 2006. LNCS, vol. 4327, pp. 29–42. Springer, Heidelberg (2006)
Laroussinie, F., Schnoebelen, P.: A Hierarchy of Temporal Logics with Past. Information and Computation 148(2), 303–324 (1995)
Laroussinie, F., Schnoebelen, P.: Specification in CTL+Past for Verification in CTL. Information and Computation 156(1-2), 236–263 (2000)
Moszkowski, B.: Temporal Logic For Multilevel Reasoning About Hardware. IEEE Computer 18(2), 10–19 (1985)
Reynolds, M.: An Axiomatization of PCTL*. Information and Computation 201(1), 72–119 (2005)
Schobbens, P.Y.: Alternating-time logic with imperfect recall. Electronic Notes in Theoretical Computer Science 85(2), 82–93 (2003); Proceedings of LCMAS 2003
Shilov, N.V., Garanina, N.O.: Model-checking Knowledge and Fixpoints. In: Preliminary Proceedings of the 3rd Workshop on Fixpoints in Computer Science (FICS 2002), number NS-02-2 in BRICS Notes Series, pp. 25–39. BRICS (July 2002) (Also available as Preprint 1998, Ershov, A.P., Institute of Informatics Systems, Russian Academy of Sciences (Siberian Division))
Thomas, W.: Infinite Trees and Automation-Definable Relations over ω-Words. Theoretical Computer Science 103(1), 143–159 (1992)
van der Hoek, W., Wooldridge, M.: Cooperation, Knowledge and Time: Alternating-time Temporal Epistemic Logic and Its Applications. Studia Logica 75, 125–157 (2003)
van der Meyden, R., Shilov, N.V.: Model Checking Knowledge And Time In Systems With Perfect Recall. In: Pandu Rangan, C., Raman, V., Ramanujam, R. (eds.) FST TCS 1999. LNCS, vol. 1738, pp. 432–445. Springer, Heidelberg (1999)
van Otterloo, S., Jonker, G.: On Epistemic Temporal Strategic Logic. In: Proceedings of the 2nd International Workshop on Logic and Communication in Multi-Agent Systems (2004). ENTCS, vol. 126, pp. 77–92. Elsevier, Amsterdam (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Guelev, D.P., Dima, C. (2009). Model-Checking Strategic Ability and Knowledge of the Past of Communicating Coalitions. In: Baldoni, M., Son, T.C., van Riemsdijk, M.B., Winikoff, M. (eds) Declarative Agent Languages and Technologies VI. DALT 2008. Lecture Notes in Computer Science(), vol 5397. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-93920-7_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-93920-7_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-93919-1
Online ISBN: 978-3-540-93920-7
eBook Packages: Computer ScienceComputer Science (R0)