×

zbMATH — the first resource for mathematics

Practical verification of multi-agent systems against Slk specifications. (English) Zbl 1395.68255
Summary: We introduce Strategy Logic with Knowledge, a novel formalism to reason about knowledge and strategic ability in memoryless multi-agent systems with incomplete information. We exemplify its expressive power; we define the model checking problem for the logic and show that it is PSpace-complete. We propose a labelling algorithm for solving the verification problem that we show is amenable to symbolic implementation. We introduce \(\mathrm{MCMAS}_{\text{\textsc{Slk}}}\), an extension of the open-source model checker MCMAS, implementing the proposed algorithm. We report the benchmarks obtained on a number of scenarios from the literature, including the dining cryptographers protocol.

MSC:
68T27 Logic in artificial intelligence
68Q60 Specification and verification (program logics, model checking, etc.)
68T42 Agent technology and artificial intelligence
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Wooldridge, M., An introduction to multiagent systems, (2009), Wiley
[2] Fagin, R.; Halpern, J. Y.; Moses, Y.; Vardi, M. Y., Reasoning about knowledge, (1995), MIT Press Cambridge · Zbl 0839.68095
[3] Lomuscio, A.; Sergot, M., Deontic interpreted systems, Stud. Log., 75, 1, 63-92, (2003) · Zbl 1033.03012
[4] Rao, A. S., Decision procedures for propositional linear-time belief-desire-intention logics, (Wooldridge, M.; Müller, J. P.; Tambe, M., Intelligent Agents II, Lect. Notes Artif. Intell., vol. 1037, (1996), Springer-Verlag Heidelberg, Germany), 33-48
[5] Pnueli, A., Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends, (de Bakker, J. W.; de Roever, W. P.; Rozenberg, G., Current Trends in Concurrency, Overviews and Tutorials, Lect. Notes Comput. Sci., vol. 224, (1986), Springer), 510-584 · Zbl 0607.68022
[6] Penczek, W.; Lomuscio, A., Verifying epistemic properties of multi-agent systems via bounded model checking, Fundam. Inform., 55, 2, 167-185, (2003) · Zbl 1111.68512
[7] Kacprzak, M.; Nabialek, W.; Niewiadomski, A.; Penczek, W.; Pólrola, A.; Szreter, M.; Wozna, B.; Zbrzezny, A., Verics 2007 — a model checker for knowledge and real-time, Fundam. Inform., 85, 1-4, 313-328, (2008) · Zbl 1167.68381
[8] Bryant, R., Graph-based algorithms for Boolean function manipulation, Trans. Comput., 35, 8, 677-691, (1986) · Zbl 0593.94022
[9] Gammie, P.; van der Meyden, R., MCK: model checking the logic of knowledge, (Proceedings of 16th International Conference on Computer Aided Verification (CAV’04), Lect. Notes Comput. Sci., vol. 3114, (2004), Springer), 479-483 · Zbl 1103.68614
[10] Raimondi, F.; Lomuscio, A., Automatic verification of multi-agent systems by model checking via OBDDs, J. Appl. Log., 5, 2, 235-251, (2005) · Zbl 1122.68076
[11] Cohen, M.; Dam, M.; Lomuscio, A.; Qu, H., A symmetry reduction technique for model checking temporal-epistemic logic, (Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI’09), Pasadena, USA, (2009)), 721-726
[12] Cohen, M.; Dam, M.; Lomuscio, A.; Russo, F., Abstraction in model checking multi-agent systems, (Proceedings of the 8th International Conference on Autonomous Agents and Multiagent Systems (AAMAS’09), (2009), IFAAMAS Press Budapest, Hungary), 945-952
[13] Lomuscio, A.; Michaliszyn, J., Verification of multi-agent systems via predicate abstraction against ATLK specifications, (Proc. of the 15th Int. Conference on Autonomous Agents and Multiagent Systems (AAMAS’16), (2016)), 662-670
[14] Alur, R.; de Alfaro, L.; Grosu, R.; Henzinger, T.; Thomas, A.; Kang, M.; Kirsch, C.; Majumdar, R.; Mang, F.; Wang, B.-Y., Jmocha: a model checking tool that exploits design structure, (Proceedings of the 23rd International Conference on Software Engineering (ICSE’01), (2001), IEEE), 835-836
[15] Hoek, W.; Wooldridge, M., Cooperation, knowledge, and time: alternating-time temporal epistemic logic and its applications, Stud. Log., 75, 1, 125-157, (2003) · Zbl 1034.03013
[16] Jamroga, W., Some remarks on alternating temporal epistemic logic, (Dunin-Kȩplicz, B.; Verbrugge, R., Proceedings of the International Workshop on Formal Approaches to Multi-Agent Systems (FAMAS’03), (2004)), 133-140
[17] Ågotnes, T.; Goranko, V.; Jamroga, W.; Wooldridge, M., Knowledge and ability, (Handbook of Logics for Knowledge and Belief, (2015), College Publications)
[18] Bulling, N.; Jamroga, W., Rational play and rational beliefs under uncertainty, (Proceedings of the 8th International Conference on Autonomous Agents and Multiagent Systems (AAMAS’16), IFAAMAS, (2009)), 257-264
[19] Lomuscio, A.; Raimondi, F., Model checking knowledge, strategies, and games in multi-agent systems, (Proceedings of the 5th International Joint Conference on Autonomous agents and Multi-Agent Systems (AAMAS’06), (2006), ACM Press), 161-168
[20] A. Lomuscio, H. Qu, F. Raimondi, MCMAS: a model checker for the verification of multi-agent systems, Software Tools for Technology Transfer.
[21] Alur, R.; Henzinger, T. A.; Kupferman, O., Alternating-time temporal logic, J. ACM, 49, 5, 672-713, (2002) · Zbl 1326.68181
[22] Jonker, G., Feasible strategies in alternating-time temporal epistemic logic, (2003), University of Utrecht The Netherlands, Master’s thesis
[23] Mogavero, F.; Murano, A.; Vardi, M., Reasoning about strategies, (Foundations of Software Technology and Theoretical Computer Science’10, LIPIcs, vol. 8, (2010), Leibniz-Zentrum fuer Informatik), 133-144 · Zbl 1245.68138
[24] Čermák, P.; Lomuscio, A.; Mogavero, F.; Murano, A., MCMAS-SLK: A model checker for the verification of strategy logic specifications, (Proceedings of the 26th International Conference on Computer Aided Verification (CAV’14), Lect. Notes Comput. Sci., vol. 8559, (2014), Springer), 525-532
[25] Chatterjee, K.; Henzinger, T.; Piterman, N., Strategy logic, Inf. Comput., 208, 6, 677-693, (2010) · Zbl 1205.68197
[26] Mogavero, F.; Murano, A.; Perelli, G.; Vardi, M., Reasoning about strategies: on the model-checking problem, Trans. Comput. Log., 15, 4, (2014), 34:1-42
[27] Alur, R.; Henzinger, T.; Kupferman, O., Alternating-time temporal logic, J. ACM, 49, 5, 672-713, (2002) · Zbl 1326.68181
[28] Fagin, R.; Halpern, J.; Moses, Y.; Vardi, M., Reasoning about knowledge, (1995), MIT Press · Zbl 0839.68095
[29] Pnueli, A., The temporal logic of programs, (Foundation of Computer Science’77, (1977), IEEE Computer Society), 46-57
[30] Lomuscio, A.; Meyden, R.; Ryan, M., Knowledge in multi-agent systems: initial configurations and broadcast, ACM Trans. Comput. Log., 1, 2, 246-282, (2000)
[31] Lomuscio, A., Knowledge sharing among ideal agents, (Jun. 1999), School of Computer Science, University of Birmingham Birmingham, UK, Ph.D. thesis
[32] Even, S.; Paz, A., A note on cake cutting, Discrete Appl. Math., 7, 285-296, (1984) · Zbl 0527.90109
[33] Kupferman, O.; Vardi, M.; Wolper, P., An automata theoretic approach to branching-time model checking, J. ACM, 47, 2, 312-360, (2000) · Zbl 1133.68376
[34] Vardi, M.; Wolper, P., An automata-theoretic approach to automatic program verification, (Logic in Computer Science’86, (1986), IEEE Computer Society), 332-344
[35] Bulling, N.; Dix, J.; Jamroga, W., Model checking logics of strategic ability: complexity, (Specification and Verification of Multi-Agent Systems’10, (2010), Springer), 125-159 · Zbl 1201.68070
[36] Stockmeyer, L.; Meyer, A., Word problems requiring exponential time (preliminary report), (Symposium on Theory of Computing’73, (1973), Association for Computing Machinery), 1-9 · Zbl 0359.68050
[37] Benerecetti, M.; Mogavero, F.; Murano, A., Reasoning about substructures and games, Trans. Comput. Log., 16, 3, (2015), 25:1-46 · Zbl 1354.03019
[38] Mogavero, F.; Murano, A.; Sauro, L., On the boundary of behavioral strategies, (Proceedings of the 28th Annual IEEE/ACM Symposium on Logic in Computer Science (LICS’13), (2013), IEEE), 263-272 · Zbl 1367.68290
[39] Lomuscio, A.; Raimondi, F., Model checking knowledge, strategies, and games in multi-agent systems, (Proceedings of the 5th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS’06), (2006), ACM Press), 161-168
[40] Morgenstern, A., Symbolic controller synthesis for LTL specifications, (2010), Ph.D. thesis
[41] Huth, M.; Ryan, M., Logic in computer science: modelling and reasoning about systems, (2004), Cambridge University Press New York, NY, USA · Zbl 1073.68001
[42] Burch, J. R.; Clarke, E. M.; McMillan, K. L.; Dill, D. L.; Hwang, L. J., Symbolic model checking: 10^{20} states and beyond, Inf. Comput., 98, 2, 142-170, (1992) · Zbl 0753.68066
[43] MCMAS-SLK - A model checker for the verification of strategy logic specifications
[44] Somenzi, F., CUDD: CU decision diagram package
[45] Lomuscio, A.; Qu, H.; Raimondi, F., MCMAS: a model checker for the verification of multi-agent systems, (Proceedings of the 21th International Conference on Computer Aided Verification (CAV’09), Lect. Notes Comput. Sci., vol. 5643, (2009), Springer), 682-688
[46] Chaum, D., The dining cryptographers problem: unconditional sender and recipient untraceability, J. Cryptol., 1, 1, 65-75, (1988) · Zbl 0654.94012
[47] van der Hoek, W.; Lomuscio, A., A logic for ignorance, Electron. Notes Theor. Comput. Sci., 85, 2, 117-133, (2004) · Zbl 1270.03042
[48] van der Meyden, R.; Su, K., Symbolic model checking the knowledge of the dining cryptographers, (Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW’04), (2004), IEEE Computer Society Washington, DC, USA), 280-291
[49] Čermák, P., A model checker for strategy logic, (2014), Department of Computing, Imperial College London, UK, Master’s thesis
[50] Chatterjee, K.; Henzinger, T. A.; Piterman, N., Strategy logic, Inf. Comput., 208, 6, 677-693, (2010) · Zbl 1205.68197
[51] Lopes, A. D.C.; Laroussinie, F.; Markey, N., ATL with strategy contexts: expressiveness and model checking, (Proceedings of the 30th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS’10), LIPIcs, vol. 8, (2010)), 120-132 · Zbl 1245.68135
[52] Huang, X.; Meyden, R.v., Symbolic model checking epistemic strategy logic, (Proceedings of the 28th Conference on Artificial Intelligence (AAAI’14), (2014), AAAI), 1426-1432
[53] Huang, X.; Meyden, R.v., A temporal logic of strategic knowledge, (Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning (KR’14), (2014), AAAI), 418-427
[54] Čermák, P.; Lomuscio, A.; Murano, A., Verifying and synthesising multi-agent systems against one-goal strategy logic specifications, (Proceedings of the 29th AAAI Conference on Artificial Intelligence (AAAI’15), (2015), AAAI Press), 2038-2044
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.