Paper published in a book (Scientific congresses, symposiums and conference proceedings)
STV+FLY: On-the-Fly Model Checking of Strategic Ability in Multi-Agent Systems
Kurpiewski, Damian; Kamiński, Mateusz; JAMROGA, Wojciech
2024 • In Endriss, Ulle (Ed.) ECAI 2024 - 27th European Conference on Artificial Intelligence, Including 13th Conference on Prestigious Applications of Intelligent Systems, PAIS 2024, Proceedings
Multiagent systems (MASs); Strategy modeling; Artificial Intelligence; Model Checking
Abstract :
[en] In this paper, we present a substantially enhanced version of our software tool STV (STrategic Verifier), dedicated to strategy synthesis and model checking of strategic abilities in multi-agent systems. The new extension, called STV+FLY, incorporates an advanced strategy synthesis algorithm that enables model checking with on-the-fly generation of the global model. This innovative approach allows for the verification of some strategic properties without generating the entire global state space, thus avoiding an important bottleneck and significantly improving the efficiency.
Disciplines :
Computer science
Author, co-author :
Kurpiewski, Damian ; Institute of Computer Science, Polish Academy of Sciences, Poland ; Faculty of Mathematics and Computer Science, Nicolaus Copernicus University in Torun, Poland
Kamiński, Mateusz ; Institute of Computer Science, Polish Academy of Sciences, Poland ; Faculty of Mathematics and Computer Science, Nicolaus Copernicus University in Torun, Poland
JAMROGA, Wojciech ; University of Luxembourg ; Institute of Computer Science, Polish Academy of Sciences, Poland
External co-authors :
yes
Language :
English
Title :
STV+FLY: On-the-Fly Model Checking of Strategic Ability in Multi-Agent Systems
Publication date :
16 October 2024
Event name :
ECAI 2024 - 27th European Conference on Artificial Intelligence
Event place :
Santiago de Compostela, Spain
Event date :
19-10-2024 => 24-10-2024
Main work title :
ECAI 2024 - 27th European Conference on Artificial Intelligence, Including 13th Conference on Prestigious Applications of Intelligent Systems, PAIS 2024, Proceedings
FNR17232062 - SpaceVote - Probabilistic Verification Of Complex Heterogeneous Systems: From Ballots To Ballistics, 2022 (01/03/2023-28/02/2026) - Peter Y. A. Ryan FNR16326754 - PABLO - Privacy-preserving Tokenisation Of Artworks, 2021 (01/06/2022-31/05/2025) - Gilbert Fridgen
Funders :
et al. Google Cloud HUAWEI IBM INDITEXTECH sdg group
Funding text :
We thank \u0141ukasz Mikulski for his comments and help in preparing the benchmark and formulas for evaluation. The work has been supported by NCBR Poland and FNR Luxembourg under the PolLux/FNR-CORE project SpaceVote (POLLUX-XI/14/SpaceVote/ 2023 and C22/IS/17232062/SpaceVote), by NCN Poland under the CHIST-ERA grant SAI (CHIST-ERA-19-XAI-010, 2020/02/Y/ST6/00064), by FNR Luxembourg under the CORE project PABLO (C21/IS/16326754/PABLO), and by the CNRS IEA project MoSART. For the purpose of open access, and in fulfilment of the obligations arising from the grant agreement, the authors have applied CC BY 4.0 license to any Author Accepted Manuscript version arising from this submission.
R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time Temporal Logic. In Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS), pages 100-109. IEEE Computer Society Press, 1997.
R. Alur, T. Henzinger, F. Mang, S. Qadeer, S. Rajamani, and S. Tasiran. MOCHA: Modularity in model checking. In Proceedings of Computer Aided Verification (CAV), volume 1427 of Lecture Notes in Computer Science, pages 521-525. Springer, 1998.
R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time Temporal Logic. Journal of the ACM, 49:672-713, 2002. doi: 10.1145/ 585265.585270.
F. Belardinelli, A. Lomuscio, A. Murano, and S. Rubin. Verification of broadcasting multi-agent systems against an epistemic strategy logic. In Proceedings of IJCAI, pages 91-97, 2017.
F. Belardinelli, A. Lomuscio, A. Murano, and S. Rubin. Verification of multi-agent systems with imperfect information and public actions. In Proceedings of AAMAS, pages 1268-1276, 2017.
F. Belardinelli, R. Condurache, C. Dima, W. Jamroga, and M. Knapik. Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol. Information and Computation, 276: 104552, 2021. doi: 10.1016/j.ic.2020.104552.
F. Belardinelli, A. Ferrando, W. Jamroga, V. Malvone, and A. Murano. Scalable verification of strategy logic through three-valued abstraction. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI, pages 46-54. ijcai.org, 2023. doi: 10.24963/IJCAI.2023/6.
N. Bulling, J. Dix, and W. Jamroga. Model checking logics of strategic ability: Complexity. In M. Dastani, K. Hindriks, and J.-J. Meyer, editors, Specification and Verification of Multi-Agent Systems, pages 125-159. Springer, 2010.
S. Busard, C. Pecheur, H. Qu, and F. Raimondi. Improving the model checking of strategies under partial observability and fairness constraints. In Formal Methods and Software Engineering, volume 8829 of Lecture Notes in Computer Science, pages 27-42. Springer, 2014. ISBN 978-3-319-11736-2. doi: 10.1007/978-3-319-11737-9_3.
P. Cermak, A. Lomuscio, F. Mogavero, and A. Murano. MCMAS-SLK: A model checker for the verification of strategy logic specifications. In Proc. of Computer Aided Verification (CAV), volume 8559 of Lecture Notes in Computer Science, pages 525-532. Springer, 2014.
P. Cermák, A. Lomuscio, and A. Murano. Verifying and synthesising multi-agent systems against one-goal strategy logic specifications. In Proceedings of AAAI, pages 2038-2044, 2015.
K. Chatterjee, T. Henzinger, and N. Piterman. Strategy Logic. Information and Computation, 208(6):677-693, 2010.
T. Chen, V. Forejt, M. Kwiatkowska, D. Parker, and A. Simaitis. PRISM-games: A model checker for stochastic multi-player games. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems (TACAS), volume 7795 of Lecture Notes in Computer Science, pages 185-191. Springer, 2013.
M. Dastani, K. Hindriks, and J. Meyer, editors. Specification and Verification of Multi-Agent Systems. Springer, 2010.
C. Dima and F. Tiplea. Model-checking ATL under imperfect information and perfect recall semantics is undecidable. CoRR, abs/1102.4225, 2011.
R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about Knowledge. MIT Press, 1995.
X. Huang and R. van der Meyden. Symbolic model checking epistemic strategy logic. In Proceedings of AAAI Conference on Artificial Intelligence, pages 1426-1432, 2014.
W. Jamroga and D. Kurpiewski. Pretty good strategies and where to find them. In Proceedings of EUMAS, volume 14282 of Lecture Notes in Computer Science, pages 363-380. Springer, 2023. doi: 10.1007/ 978-3-031-43264-4\_23.
W. Jamroga, M. Knapik, and D. Kurpiewski. Model checking the SELENE e-voting protocol in multi-agent logics. In Proceedings of the 3rd International Joint Conference on Electronic Voting (E-VOTE-ID), volume 11143 of Lecture Notes in Computer Science, pages 100-116. Springer, 2018.
W. Jamroga, W. Penczek, P. Dembiński, and A. Mazurkiewicz. Towards partial order reductions for strategic ability. In Proceedings of the 17th International Conference on Autonomous Agents and Multiagent Systems (AAMAS), pages 156-165. IFAAMAS, 2018.
W. Jamroga, M. Knapik, D. Kurpiewski, and Ł. Mikulski. Approximate verification of strategic abilities under imperfect information. Artificial Intelligence, 277, 2019. doi: 10.1016/j.artint.2019.103172.
W. Jamroga, Y. Kim, D. Kurpiewski, and P. Y. A. Ryan. Towards model checking of voting protocols in uppaal. In Proceedings of E-Vote-ID, volume 12455 of Lecture Notes in Computer Science, pages 129-146. Springer, 2020. doi: 10.1007/978-3-030-60347-2\_9.
W. Jamroga, W. Penczek, T. Sidoruk, P. Dembiński, and A. Mazurkiewicz. Towards partial order reductions for strategic ability. Journal of Artificial Intelligence Research, 68:817-850, 2020. doi: 10.1613/jair.1.11936.
W. Jamroga, D. Kurpiewski, and V. Malvone. Natural strategic abilities in voting protocols. In Proceedings of STAST 2020, 2021. To appear.
W. Jamroga, W. Penczek, and T. Sidoruk. Strategic abilities of asynchronous agents: Semantic side effects and how to tame them. In Proceedings of KR 2021, pages 368-378, 2021.
M. Kaminski, D. Kurpiewski, and W. Jamroga. STV+KH: towards practical verification of strategic ability for knowledge and information flow. In Proceedings of AAMAS, pages 2812-2814. ACM, 2024. doi: 10.5555/3635637.3663296.
D. Kurpiewski, W. Jamroga, and M. Knapik. STV: Model checking for strategies under imperfect information. In Proceedings of the 18th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2019, pages 2372-2374. IFAAMAS, 2019.
D. Kurpiewski, M. Knapik, and W. Jamroga. On domination and control in strategic ability. In Proceedings of the 18th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2019, pages 197-205. IFAAMAS, 2019.
D. Kurpiewski, W. Pazderski, W. Jamroga, and Y. Kim. STV+Reductions: Towards practical verification of strategic ability using model reductions. In Proceedings of AAMAS, pages 1770-1772. ACM, 2021.
D. Kurpiewski, W. Jamroga, L. Masko, L. Mikulski, W. Pazderski, W. Penczek, and T. Sidoruk. Verification of multi-agent properties in electronic voting: A case study. In Advances in Modal Logic, pages 531-556. College Publications, 2022.
A. Lomuscio, B. Strulo, N. G. Walker, and P. Wu. Assume-guarantee reasoning with local specifications. Int. J. Found. Comput. Sci., 24(4): 419-444, 2013. doi: 10.1142/S0129054113500123.
A. Lomuscio, H. Qu, and F. Raimondi. MCMAS: An open-source model checker for the verification of multi-agent systems. International Journal on Software Tools for Technology Transfer, 19(1):9-30, 2017. doi: 10.1007/s10009-015-0378-x.
L. Mikulski, W. Jamroga, and D. Kurpiewski. Assume-guarantee verification of strategic ability. In Proceedings of PRIMA, volume 13753 of Lecture Notes in Computer Science, pages 173-191. Springer, 2022. doi: 10.1007/978-3-031-21203-1\_11.
F. Mogavero, A. Murano, G. Perelli, and M. Vardi. Reasoning about strategies: On the model-checking problem. ACM Transactions on Computational Logic, 15(4):1-42, 2014.
P. Ryan. The computer ate my vote. In Formal Methods: State of the Art and New Directions, pages 147-184. Springer, 2010.
P. Ryan, P. Rønne, and V. Iovino. Selene: Voting with transparent verifiability and coercion-mitigation. In Financial Cryptography and Data Security: Proceedings of FC 2016. Revised Selected Papers, volume 9604 of Lecture Notes in Computer Science, pages 176-192. Springer, 2016. doi: 10.1007/978-3-662-53357-4\_12.
P. Y. Schobbens. Alternating-time logic with imperfect recall. Electronic Notes in Theoretical Computer Science, 85(2):82-93, 2004.
M. Tabatabaei, W. Jamroga, and P. Y. A. Ryan. Expressing receipt-freeness and coercion-resistance in logics of strategic ability: Preliminary attempt. In Proceedings of the 1st International Workshop on AI for Privacy and Security, PrAISe@ECAI 2016, pages 1:1-1:8. ACM, 2016. doi: 10.1145/2970030.2970039.
