Abstract
We present a technique for verifying strategic abilities of multi-agent systems via SAT-based bounded model checking. In our approach we focus on systems of agents that pursue goals with regard to the allocation of shared resources. The problem to be solved is to determine whether a coalition of agents has a joint strategy that guarantees the achievement of all resource goals, irrespective of how the opposing agents in the system act. Our approach does not only decide whether such a strategy exists, but also synthesises the strategy. The technique is based on a propositional logic encoding of the model checking problem. The encoding is satisfiable if and only if some specified coalition of agents has a strategy to reach a resource allocation goal. Each satisfying truth assignment of the encoding characterises a successful strategy.
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
Similar content being viewed by others
References
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM (JACM) 49(5), 672–713 (2002)
Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, S.K., Tasiran, S.: MOCHA: modularity in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 521–525. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0028774
Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)
Biere, A.: PicoSAT essentials. J. Satisf. Boolean Model. Comput. 4(2–4), 75–97 (2008)
Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. In: Handbook of Satisfiability, vol. 185, no. 99, pp. 457–481 (2009)
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NUSMV: a new symbolic model checker. STTT 2(4), 410–425 (2000). https://doi.org/10.1007/s100090050046
Cohen, M., Dam, M., Lomuscio, A., Qu, H.: A symmetry reduction technique for model checking temporal-epistemic logic. In: IJCAI (2009)
De Masellis, R., Goranko, V., Gruner, S., Timm, N.: Generalising the dining philosophers problem: competitive dynamic resource allocation in multi-agent systems. In: Slavkovik, M. (ed.) EUMAS 2018. LNCS (LNAI), vol. 11450, pp. 30–47. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-14174-5_3
Jamroga, W., Penczek, W., Sidoruk, T., Dembiński, P., Mazurkiewicz, A.: Towards partial order reductions for strategic ability. JAIR 68, 817–850 (2020)
Kacprzak, M., Penczek, W.: Unbounded model checking for alternating-time temporal logic. In: CAV, pp. 646–653. IEEE (2004)
Kroening, D., Ouaknine, J., Strichman, O., Wahl, T., Worrell, J.: Linear completeness thresholds for bounded model checking. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 557–572. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_44
Lomuscio, A., Penczek, W., Woźna, B.: Bounded model checking for knowledge and real time. Artif. Intell. 171(16–17), 1011–1038 (2007)
Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: an open-source model checker for the verification of multi-agent systems. STTT 19(1), 9–30 (2017). https://doi.org/10.1007/s10009-015-0378-x
Luo, X., Su, K., Sattar, A., Reynolds, M.: Verification of multi-agent systems via bounded model checking. In: Sattar, A., Kang, B. (eds.) AI 2006. LNCS (LNAI), vol. 4304, pp. 69–78. Springer, Heidelberg (2006). https://doi.org/10.1007/11941439_11
Pilecki, J., Bednarczyk, M.A., Jamroga, W.: SMC: synthesis of uniform strategies and verification of strategic ability for multi-agent systems. J. Log. Comput. 27(7), 1871–1895 (2017)
Raimondi, F., Lomuscio, A.: Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams. J. Appl. Log. 5(2), 235–251 (2007)
Schewe, S.: ATL* satisfiability is 2EXPTIME-complete. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008. LNCS, vol. 5126, pp. 373–385. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70583-3_31
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Timm, N., Botha, J. (2021). Model Checking and Strategy Synthesis for Multi-agent Systems for Resource Allocation. In: Campos, S., Minea, M. (eds) Formal Methods: Foundations and Applications. SBMF 2021. Lecture Notes in Computer Science(), vol 13130. Springer, Cham. https://doi.org/10.1007/978-3-030-92137-8_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-92137-8_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-92136-1
Online ISBN: 978-3-030-92137-8
eBook Packages: Computer ScienceComputer Science (R0)