zbMATH — the first resource for mathematics

Specification and verification of multi-agent systems. (English) Zbl 1250.68190
Bezhanishvili, Nick (ed.) et al., Lectures on logic and computation. ESSLLI 2010 Copenhagen, Denmark, August 2010, ESSLLI 2011, Ljubljana, Slovenia, August 2011. Selected lecture notes. Berlin: Springer (ISBN 978-3-642-31484-1/pbk). Lecture Notes in Computer Science 7388, 210-263 (2012).
From the introduction: Multi-agent systems (MAS) provide an important framework for formalizing various problems in computer science, artificial intelligence, game theory, social choice theory, etc. Modal logics are amongst the most suitable and versatile logical formalisms for specification and verification of computational systems. Here, we present an overview of some important developments in the area. We introduce modal logics used for specification of temporal, epistemic, and strategic properties of systems; then we present some model-checking algorithms, and discuss the computational complexity of the model-checking problem. Finally, we consider symbolic (compact) representations of systems based on binary decision diagrams (BDD) and propositional logic formulas, and show how the representations change the algorithmic side of model checking. We also discuss other techniques that help to reduce the complexity and make the verification feasible even for large systems.
For the entire collection see [Zbl 1248.03007].

68Q60 Specification and verification (program logics, model checking, etc.)
03B45 Modal logic (including the logic of norms)
68T27 Logic in artificial intelligence
68T42 Agent technology and artificial intelligence
91A99 Game theory
91B14 Social choice
Full Text: DOI
[1] Ågotnes, T.: Action and knowledge in alternating-time temporal logic. Synthese 149(2), 377–409 (2006); Section on Knowledge, Rationality and Action · Zbl 1107.03013 · doi:10.1007/s11229-005-3875-8
[2] Ågotnes, T., Goranko, V., Jamroga, W.: Alternating-time temporal logics with irrevocable strategies. In: Samet, D. (ed.) Proceedings of TARK XI, pp. 15–24 (2007) · doi:10.1145/1324249.1324256
[3] Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time Temporal Logic. In: Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS), pp. 100–109. IEEE Computer Society Press (1997) · Zbl 1326.68181 · doi:10.1109/SFCS.1997.646098
[4] Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time Temporal Logic. Journal of the ACM 49, 672–713 (2002) · Zbl 1326.68181 · doi:10.1145/585265.585270
[5] Beeri, C.: On the membership problem for functional and multivalued dependencies in relational databases. ACM Transactions on Database Systems 5(3), 241–259 (1980) · Zbl 0441.68118 · doi:10.1145/320613.320614
[6] Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded model checking. In: Highly Dependable Software. Advances in Computers, vol. 58. Academic Press (2003) (pre-print) · doi:10.1016/S0065-2458(03)58003-2
[7] Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science, vol. 53. Cambridge University Press (2001) · Zbl 0988.03006
[8] Bulling, N.: Model checking coalition logic on implicit models is \(\Delta\)3-complete. Technical Report IfI-10-02, Clausthal University of Technology (2010)
[9] Bulling, N., Dix, J., Jamroga, W.: Model checking logics of strategic ability: Complexity. In: Dastani, M., Hindriks, K., Meyer, J.-J. (eds.) Specification and Verification of Multi-Agent Systems, pp. 125–159. Springer (2010) · Zbl 1201.68070 · doi:10.1007/978-1-4419-6984-2_5
[10] Bulling, N., Jamroga, W.: What agents can probably enforce. Fundamenta Informaticae 93(1-3), 81–96 (2009) · Zbl 1191.68648
[11] Bulling, N., Jamroga, W.: Alternating epistemic mu-calculus. In: Proceedings of IJCAI 2011, pp. 109–114 (2011)
[12] Bulling, N., Jamroga, W., Dix, J.: Reasoning about temporal properties of rational play. Annals of Mathematics and Artificial Intelligence 53(1-4), 51–114 (2008) · Zbl 1187.03016 · doi:10.1007/s10472-009-9110-4
[13] Clarke, E., Emerson, E.A., Sistla, A.P.: Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. ACM Transactions on Programming Languages and Systems 8(2), 244–263 (1986) · Zbl 0591.68027 · doi:10.1145/5397.5399
[14] Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8(2), 244–263 (1986) · Zbl 0591.68027 · doi:10.1145/5397.5399
[15] Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)
[16] Cohen, P.R., Levesque, H.J.: Intention is choice with commitment. Artificial Intelligence 42, 213–261 (1990) · Zbl 0721.03017 · doi:10.1016/0004-3702(90)90055-5
[17] Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Journal of the ACM 5(7), 394–397 (1962) · Zbl 0217.54002 · doi:10.1145/368273.368557
[18] Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7(3), 201–215 (1960) · Zbl 0212.34203 · doi:10.1145/321033.321034
[19] de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: Model checking discounted temporal properties. Theoretical Computer Science 345, 139–170 (2005) · Zbl 1079.68062 · doi:10.1016/j.tcs.2005.07.033
[20] Dembinski, P., Janowska, A., Janowski, P., Penczek, W., Półrola, A., Szreter, M., Woźna, B., Zbrzezny, A.: \(\surd\) erics: A Tool for Verifying Timed Automata and Estelle Specifications. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 278–283. Springer, Heidelberg (2003) · Zbl 1031.68546 · doi:10.1007/3-540-36577-X_20
[21] Dima, C., Tiplea, F.L.: Model-checking atl under imperfect information and perfect recall semantics is undecidable. CoRR, abs/1102.4225 (2011)
[22] Doyen, L., Raskin, J.-F.: Games with imperfect information: Theory and algorithms. Lecture Notes in Game Theory for Computer Scientists, pp. 185–212. Cambridge University Press (2011) · Zbl 1229.91080 · doi:10.1017/CBO9780511973468.007
[23] Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 995–1072. Elsevier Science Publishers (1990) · Zbl 0900.03030 · doi:10.1016/B978-0-444-88074-1.50021-4
[24] Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional mu-calculus. In: Proc. of the 1st Symp. on Logic in Computer Science (LICS 1986), pp. 267–278. IEEE Computer Society (1986)
[25] Emerson, E.A., Lei, C.-L.: Modalities for model checking: Branching time logic strikes back. Science of Computer Programming 8(3), 275–306 (1987) · Zbl 0615.68019 · doi:10.1016/0167-6423(87)90036-0
[26] Emerson, E.A., Sistla, A.P.: Deciding branching time logic. In: STOC 1984: Proceedings of the Sixteenth Annual ACM Symposium on Theory of Computing, pp. 14–24. ACM, New York (1984) · Zbl 0593.03007 · doi:10.1145/800057.808661
[27] Emerson, E.A., Halpern, J.Y.: ”sometimes” and ”not never” revisited: On branching versus linear time temporal logic. Journal of the ACM 33(1), 151–178 (1986) · Zbl 0629.68020 · doi:10.1145/4904.4999
[28] Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press (1995) · Zbl 0839.68095
[29] Fisher, M.: Temporal Logics. Kluwer (2006) · Zbl 1236.68224
[30] Fitting, M.: First-Order Logic and Automated Theorem Proving. Springer (1990) · Zbl 0692.68002 · doi:10.1007/978-1-4684-0357-2
[31] Furst, M., Saxe, J.B., Sipser, M.: Parity, circuits, and the polynomial-time hierarchy. Math. Systems Theory 17, 13–27 (1984) · Zbl 0534.94008 · doi:10.1007/BF01744431
[32] Goranko, V., Jamroga, W.: State and path effectivity models for logics of multi-player games. In: Proceedings of AAMAS (to appear, 2012)
[33] Goranko, V., Jamroga, W., Turrini, P.: Strategic games and truly playable effectivity functions. In: Proceedings of AAMAS 2011, pp. 727–734 (2011)
[34] Goranko, V., van Drimmelen, G.: Complete axiomatization and decidability of alternating-time temporal logic. Theoretical Computer Science 353(1), 93–117 (2006) · Zbl 1089.03013 · doi:10.1016/j.tcs.2005.07.043
[35] Guelev, D.P., Dima, C., Enea, C.: An alternating-time temporal logic with knowledge, perfect recall and past: axiomatisation and model-checking. Journal of Applied Non-Classical Logics 21(1), 93–131 (2011) · Zbl 1242.68161 · doi:10.3166/jancl.21.93-131
[36] Halpern, J.Y.: Reasoning about knowledge: a survey. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) The Handbook of Logic in Artificial Intelligence and Logic Programming, vol. IV, pp. 1–34. Oxford University Press (1995)
[37] Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000) · Zbl 0976.68108
[38] Harrenstein, B.P., van der Hoek, W., Meyer, J.-J., Witteveen, C.: A modal characterization of Nash equilibrium. Fundamenta Informaticae 57(2-4), 281–321 (2003) · Zbl 1041.03016
[39] Harrenstein, P., van der Hoek, W., Meijer, J.-J., Witteveen, C.: Subgame-perfect Nash equilibria in dynamic logic. In: Pauly, M., Baltag, A. (eds.) Proceedings of the ILLC Workshop on Logic and Games, vol. 25, pp. 29–30. University of Amsterdam (2002); Tech. Report PP-1999-25
[40] Hawke, P.: Coordination, almost perfect information and strategic ability. In: Proceedings of LAMAS (2010)
[41] van der Hoek, W., Wooldridge, M.: Model Checking Knowledge and Time. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 95–111. Springer, Heidelberg (2002) · Zbl 1077.68708 · doi:10.1007/3-540-46017-9_9
[42] Huang, X., Su, K., Zhang, C.: Probabilistic alternating-time temporal logic of incomplete information and synchronous perfect recall. In: Proceedings of AAAI 2012 (to appear, 2012)
[43] Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press (2004) · Zbl 1073.68001 · doi:10.1017/CBO9780511810275
[44] Immerman, N.: Number of quantifiers is better than number of tape cells. Journal of Computer and System Sciences 22(3), 384–406 (1981) · Zbl 0486.03019 · doi:10.1016/0022-0000(81)90039-8
[45] Jamroga, W.: Some remarks on alternating temporal epistemic logic. In: Dunin-Keplicz, B., Verbrugge, R. (eds.) Proceedings of Formal Approaches to Multi-Agent Systems (FAMAS 2003), pp. 133–140 (2003)
[46] Jamroga, W.: A Temporal Logic for Stochastic Multi-Agent Systems. In: Bui, T.D., Ho, T.V., Ha, Q.T. (eds.) PRIMA 2008. LNCS (LNAI), vol. 5357, pp. 239–250. Springer, Heidelberg (2008) · Zbl 05488370 · doi:10.1007/978-3-540-89674-6_27
[47] Jamroga, W.: Easy Yet Hard: Model Checking Strategies of Agents. In: Fisher, M., Sadri, F., Thielscher, M. (eds.) CLIMA IX. LNCS, vol. 5405, pp. 1–12. Springer, Heidelberg (2009) · Zbl 1250.68189 · doi:10.1007/978-3-642-02734-5_1
[48] Jamroga, W., Ågotnes, T.: Modular interpreted systems: A preliminary report. Technical Report IfI-06-15, Clausthal University of Technology (2006)
[49] Jamroga, W., Ågotnes, T.: Constructive knowledge: What agents can achieve under incomplete information. Journal of Applied Non-Classical Logics 17(4), 423–475 (2007) · Zbl 1186.03031 · doi:10.3166/jancl.17.423-475
[50] Jamroga, W., Ågotnes, T.: Modular interpreted systems. In: Proceedings of AAMAS 2007, pp. 892–899 (2007) · doi:10.1145/1329125.1329286
[51] Jamroga, W., Dix, J.: Do Agents Make Model Checking Explode (Computationally)? In: Pěchouček, M., Petta, P., Varga, L.Z. (eds.) CEEMAS 2005. LNCS (LNAI), vol. 3690, pp. 398–407. Springer, Heidelberg (2005) · doi:10.1007/11559221_40
[52] Jamroga, W., Dix, J.: Model checking ATL ir is indeed \(\Delta_2^P\) -complete. In: Proceedings of EUMAS 2006 (2006)
[53] Jamroga, W., Dix, J.: Model checking abilities of agents: A closer look. Theory of Computing Systems 42(3), 366–410 (2008) · Zbl 1136.68036 · doi:10.1007/s00224-007-9080-z
[54] Jamroga, W., van der Hoek, W.: Agents that know how to play. Fundamenta Informaticae 63(2-3), 185–219 (2004) · Zbl 1102.68106
[55] Jonker, G.: Feasible strategies in Alternating-time Temporal Epistemic Logic. Master thesis, University of Utrecht (2003)
[56] Kacprzak, M., Lomuscio, A., Łasica, T., Penczek, W., Szreter, M.: Verifying Multi-agent Systems via Unbounded Model Checking. In: Hinchey, M.G., Rash, J.L., Truszkowski, W.F., Rouff, C.A. (eds.) FAABS 2004. LNCS (LNAI), vol. 3228, pp. 189–212. Springer, Heidelberg (2004) · doi:10.1007/978-3-540-30960-4_13
[57] Kacprzak, M., Lomuscio, A., Niewiadomski, A., Penczek, W., Raimondi, F., Szreter, M.: Comparing BDD and SAT based techniques for model checking Chaum’s dining cryptographers protocol. Fundamenta Informaticae 72(1-2), 215–234 (2006) · Zbl 1097.68074
[58] Kacprzak, M., Lomuscio, A., Penczek, W.: From bounded to unbounded model checking for temporal epistemic logic. Fundamenta Informaticae 63(2-3), 221–240 (2004) · Zbl 1102.68107
[59] Kacprzak, M., Lomuscio, A., Penczek, W.: From bounded to unbounded model checking for temporal epistemic logic. Fundam. Inform. 63(2-3), 221–240 (2004) · Zbl 1102.68107
[60] Kacprzak, M., Nabialek, W., Niewiadomski, A., Penczek, W., Pólrola, A., Szreter, M., Woźna, B., Zbrzezny, A.: VerICS 2007 - a model checker for knowledge and real-time. Fundamenta Informaticae 85(1-4), 313–328 (2008) · Zbl 1167.68381
[61] Kacprzak, M., Penczek, W.: Fully symbolic unbounded model checking for alternating-time temporal logic. Autonomous Agents and Multi-Agent Systems 11(1), 69–89 (2005) · Zbl 05387330 · doi:10.1007/s10458-005-0944-9
[62] Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science 27, 333–354 (1983) · Zbl 0553.03007 · doi:10.1016/0304-3975(82)90125-6
[63] Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. Journal of the ACM 47(2), 312–360 (2000) · Zbl 1133.68376 · doi:10.1145/333979.333987
[64] Laroussinie, F., Markey, N., Oreiby, G.: On the expressiveness and complexity of ATL. Logical Methods in Computer Science 4, 7 (2008) · Zbl 1143.68044 · doi:10.2168/LMCS-4(2:7)2008
[65] Laroussinie, F., Markey, N., Schnoebelen, P.: Model Checking CTL + and FCTL is Hard. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, pp. 318–331. Springer, Heidelberg (2001) · Zbl 0986.68067 · doi:10.1007/3-540-45315-6_21
[66] Leyton-Brown, K., Shoham, Y.: Essentials of Game Theory: A Concise, Multidisciplinary Introduction. Morgan & Claypool (2008) · Zbl 1203.91002
[67] Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: POPL 1985: Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 97–107. ACM, New York (1985)
[68] Lomuscio, A., Penczek, W.: Logic column 19: Symbolic model checking for temporal-epistemic logics. CoRR, abs/0709.0446 (2007)
[69] Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: A Model Checker for the Verification of Multi-Agent Systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 682–688. Springer, Heidelberg (2009) · Zbl 05571936 · doi:10.1007/978-3-642-02658-4_55
[70] Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proc. of the 38th Design Automation Conference (DAC 2001), pp. 530–535 (June 2001) · doi:10.1145/378239.379017
[71] Osborne, M., Rubinstein, A.: A Course in Game Theory. MIT Press (1994) · Zbl 1194.91003
[72] Papadimitriou, C.H.: Computational Complexity. Addison Wesley, Reading (1994) · Zbl 0833.68049
[73] Pauly, M.: Logic for Social Software. PhD thesis, University of Amsterdam (2001)
[74] Penczek, W., Lomuscio, A.: Verifying epistemic properties of multi-agent systems via bounded model checking. In: Proc. of the 2nd Int. Conf. on Autonomous Agents and Multi-Agent Systems (AAMAS 2003), pp. 209–216. ACM (2003) · Zbl 1111.68512 · doi:10.1145/860575.860609
[75] Penczek, W., Lomuscio, A.: Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae 55(2), 167–185 (2003) · Zbl 1111.68512
[76] Penczek, W., Polrola, A.: Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach. SCI, vol. 20. Springer (2006) · Zbl 1110.68087 · doi:10.1007/978-3-540-32870-4
[77] Peterson, G., Reif, J.: Multiple-person alternation. In: Proceedings of the 20th Annual Symposium on Foundations of Computer Science (FOCS), pp. 348–363. IEEE Computer Society Press (1979) · doi:10.1109/SFCS.1979.25
[78] Peterson, G., Reif, J., Azhar, S.: Lower bounds for multiplayer noncooperative games of incomplete information. Computers and Mathematics with Applications 41(7), 957–992 · Zbl 0991.91007 · doi:10.1016/S0898-1221(00)00333-3
[79] Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL 1989: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 179–190. ACM, New York (1989) · Zbl 0686.68015
[80] Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Proceedings of the 31th Annual Symposium on Foundations of Computer Science (FOCS), pp. 746–757. IEEE Computer Society Press (1990) · doi:10.1109/FSCS.1990.89597
[81] Raimondi, F.: Model Checking Multi-Agent Systems. PhD thesis, University College London (2006)
[82] Raimondi, F., Lomuscio, A.: Automatic verification of deontic interpreted systems by model checking via OBDD’s. In: de Mántaras, R.L., Saitta, L. (eds.) Proceedings of ECAI, pp. 53–57 (2004)
[83] Raimondi, F., Lomuscio, A.: Verification of multiagent systems via ordered binary decision diagrams: An algorithm and its implementation. In: AAMAS, pp. 630–637 (2004)
[84] Rao, A.S., Georgeff, M.P.: Modeling rational agents within a BDI-architecture. In: Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning, pp. 473–484 (1991) · Zbl 0765.68194
[85] Rosner, R.: Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science (1992)
[86] Schnoebelen, P.: The complexity of temporal model checking. In: Advances in Modal Logics, Proceedings of AiML 2002. World Scientific (2003)
[87] Schnoor, H.: Strategic planning for probabilistic games with incomplete information. In: Proceedings of AAMAS 2010, pp. 1057–1064 (2010)
[88] Schobbens, P.Y.: Alternating-time logic with imperfect recall. Electronic Notes in Theoretical Computer Science 85(2), 82–93 (2004) · Zbl 1270.68287 · doi:10.1016/S1571-0661(05)82604-0
[89] Sheeran, M., Singh, S., Stålmarck, G.: Checking Safety Properties Using Induction and a SAT-Solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000) · doi:10.1007/3-540-40922-X_8
[90] Shilov, N.V., Garanina, N.O., Choe, K.-M.: Update and abstraction in model checking of knowledge and branching time. Fundamenta Informaticae 72(1-3), 347–361 (2006) · Zbl 1097.68077
[91] Shilov, N.V., Garanina, N.O., Kalinina, N.A.: Model checking knowledge, actions and fixpoints. In: Proceedings of CS&P 2004, pp. 351–357 (2004)
[92] Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. Journal of ACM 32(3), 733–749 (1985) · Zbl 0632.68034 · doi:10.1145/3828.3837
[93] Stirling, C.: Modal and Temporal Properties of Processes. Springer (2001) · Zbl 0981.68114 · doi:10.1007/978-1-4757-3550-5
[94] Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics 5, 285–309 (1955) · Zbl 0064.26004 · doi:10.2140/pjm.1955.5.285
[95] van der Hoek, W., Jamroga, W., Wooldridge, M.: A logic for strategic reasoning. In: Proceedings of AAMAS 2005, pp. 157–164 (2005) · doi:10.1145/1082473.1082497
[96] van der Hoek, W., Lomuscio, A., Wooldridge, M.: On the complexity of practical ATL model checking. In: Stone, P., Weiss, G. (eds.) Proceedings of AAMAS 2006, pp. 201–208 (2006) · doi:10.1145/1160633.1160665
[97] van der Hoek, W., Verbrugge, R.: Epistemic logic: A survey. Game Theory and Applications 8, 53–94 (2002) · Zbl 1034.03517
[98] van der Hoek, W., Wooldridge, M.: Tractable multiagent planning for epistemic goals. In: Castelfranchi, C., Johnson, W.L. (eds.) Proceedings of the First International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2002), pp. 1167–1174. ACM Press, New York (2002) · doi:10.1145/545056.545095
[99] 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) · Zbl 1034.03013 · doi:10.1023/A:1026185103185
[100] van der Meyden, R., Shilov, N.V.: Model Checking Knowledge and Time in Systems with Perfect Recall (Extended Abstract). In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FST TCS 1999. LNCS, vol. 1738, pp. 432–445. Springer, Heidelberg (1999) · Zbl 0958.68119 · doi:10.1007/3-540-46691-6_35
[101] van Otterloo, S., Jonker, G.: On Epistemic Temporal Strategic Logic. Electronic Notes in Theoretical Computer Science XX, 35–45 (2004); Proceedings of LCMAS 2004 · Zbl 1272.68384
[102] Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986), pp. 332–344. IEEE Computer Society Press (1986)
[103] Walther, D., van der Hoek, W., Wooldridge, M.: Alternating-time temporal logic with explicit strategies. In: Samet, D. (ed.) Proceedings TARK XI, pp. 269–278. Presses Universitaires de Louvain (2007) · doi:10.1145/1324249.1324285
[104] Weiss, G. (ed.): Multiagent Systems. A Modern Approach to Distributed Artificial Intelligence. MIT Press, Cambridge (1999)
[105] Wooldridge, M.: An Introduction to Multi Agent Systems. John Wiley & Sons (2002)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.