Cited By
View all- Briola DFerrando AMascardi V(2023)Fantastic MASs and Where to Find Them: First Results and Lesson LearnedEngineering Multi-Agent Systems10.1007/978-3-031-48539-8_16(233-252)Online publication date: 29-May-2023
STV+Reductions: Towards Practical Verification of Strategic Ability Using Model Reductions
Pages 1770 - 1772
Abstract
We present a substantially expanded version of our tool STV for strategy synthesis and verification of strategic abilities. The new version adds user-definable models and support for model reduction through partial order reduction and checking for bisimulation.
References
[1]
R. Alur, L. de Alfaro, R. Grossu, T.A. Henzinger, M. Kang, C.M. Kirsch, R. Majumdar, F.Y.C. Mang, and B.-Y. Wang. 2001. jMocha: A Model-Checking Tool that Exploits Design Structure. In Proceedings of International Conference on Software Engineering (ICSE). IEEE Computer Society Press, 835--836.
[2]
R. Alur, T. Henzinger, F. Mang, S. Qadeer, S. Rajamani, and S. Tasiran. 1998.MOCHA: Modularity in Model Checking. In Proceedings of Computer Aided Verification (CAV) (Lecture Notes in Computer Science, Vol. 1427). Springer, 521--525.
[3]
R. Alur, T. A. Henzinger, and O. Kupferman. 1997. Alternating-Time Temporal Logic. In Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS). IEEE Computer Society Press, 100--109.
[4]
R. Alur, T. A. Henzinger, and O. Kupferman. 2002. Alternating-Time Temporal Logic. J. ACM 49 (2002), 672--713. https://doi.org/10.1145/585265.585270
[5]
C. Baier and J.-P. Katoen. 2008. Principles of Model Checking. MIT Press.
[6]
Francesco Belardinelli, Rodica Condurache, Catalin Dima, Wojciech Jamroga,and Michal Knapik. 2021. Bisimulations for verifying strategic abilities with an application to the Three Ballot voting protocol. Information and Computation 276 (2021), 104552. https://doi.org/10.1016/j.ic.2020.104552
[7]
F. Belardinelli, A. Lomuscio, A. Murano, and S. Rubin. 2017. Verification of Broad-casting Multi-Agent Systems against an Epistemic Strategy Logic. In Proceedings of IJCAI. 91--97.
[8]
F. Belardinelli, A. Lomuscio, A. Murano, and S. Rubin. 2017. Verification of Multi-agent Systems with Imperfect Information and Public Actions. In Proceedings of AAMAS. 1268--1276.
[9]
N. Bulling, J. Dix, and W. Jamroga. 2010. Model Checking Logics of Strategic Ability: Complexity. In Specification and Verification of Multi-Agent Systems, M. Dastani, K. Hindriks, and J.-J. Meyer (Eds.). Springer, 125--159.
[10]
N. Bulling and W. Jamroga. 2011. Alternating Epistemic Mu-Calculus. In Proceedings of IJCAI-11. 109--114.
[11]
S. Busard, C. Pecheur, H. Qu, and F. Raimondi. 2014. Improving the Model Checking of Strategies under Partial Observability and Fairness Constraints. In Formal Methods and Software Engineering. Lecture Notes in Computer Science, Vol. 8829. Springer, 27--42. https://doi.org/10.1007/978--3--319--11737--9_3
[12]
S. Busard, C. Pecheur, H. Qu, and F. Raimondi. 2015. Reasoning about memory-less strategies under partial observability and unconditional fairness constraints.Information and Computation 242 (2015), 128--156. https://doi.org/10.1016/j.ic.2015.03.014
[13]
P. Cermak, A. Lomuscio, F. Mogavero, and A. Murano. 2014. MCMAS-SLK: AModel Checker for the Verification of Strategy Logic Specifications. In Proc. of Computer Aided Verification (CAV) (Lecture Notes in Computer Science, Vol. 8559). Springer, 525--532.
[14]
Petr Cermák, Alessio Lomuscio, and Aniello Murano. 2015. Verifying and Synthesising Multi-Agent Systems against One-Goal Strategy Logic Specifications. In Proceedings of AAAI. 2038--2044.
[15]
T. Chen, V. Forejt, M. Kwiatkowska, D. Parker, and A. Simaitis. 2013. PRISM-games: A Model Checker for Stochastic Multi-Player Games. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems (TACAS) (Lecture Notes in Computer Science, Vol. 7795). Springer, 185--191.
[16]
C. Dima, B. Maubert, and S. Pinchinat. 2014. The Expressive Power of Epistemicu-Calculus. CoRRabs/1407.5166 (2014).
[17]
C. Dima, B. Maubert, and S. Pinchinat. 2015. Relating Paths in Transition Systems: The Fall of the Modal Mu-Calculus. In Proceedings of Mathematical Foundations of Computer Science (MFCS) (Lecture Notes in Computer Science, Vol. 9234). Springer, 179--191.https://doi.org/10.1007/978--3--662--48057--1_14
[18]
C. Dima and F.L. Tiplea. 2011. Model-checking ATL under Imperfect Information and Perfect Recall Semantics is Undecidable. CoRRabs/1102.4225 (2011).
[19]
R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. 1995. Reasoning about Knowledge. MIT Press.
[20]
D.P. Guelev, C. Dima, and C. Enea. 2011. An alternating-time temporal logic with knowledge, perfect recall and past: axiomatisation and model-checking. Journal of Applied Non-Classical Logics21, 1 (2011), 93--131.
[21]
X. Huang and R. van der Meyden. 2014. Symbolic Model Checking Epistemic Strategy Logic. In Proceedings of AAAI Conference on Artificial Intelligence. 1426--1432.
[22]
W. Jamroga and J. Dix. 2006. Model Checking ATLiris Indeed?P2-complete. In Proceedings of EUMAS (CEUR Workshop Proceedings, Vol. 223).
[23]
Wojciech Jamroga, Yan Kim, Damian Kurpiewski, and Peter Y. A. Ryan. 2020. Towards Model Checking of Voting Protocols in Uppaal. In Proceedings of E-Vote-ID (Lecture Notes in Computer Science, Vol. 12455). Springer, 129--146. https://doi.org/10.1007/978--3-030--60347--2_9
[24]
W. Jamroga, M. Knapik, and D. Kurpiewski. 2017. Fixpoint Approximation of Strategic Abilities under Imperfect Information. In Proceedings of the 16th International Conference on Autonomous Agents and Multiagent Systems (AAMAS). IFAAMAS, 1241--1249.
[25]
W. Jamroga, M. Knapik, and D. Kurpiewski. 2018. Model Checking the SELENEE-Voting Protocol in Multi-Agent Logics. In Proceedings of the 3rd International Joint Conference on Electronic Voting (E-VOTE-ID) (Lecture Notes in Computer Science, Vol. 11143). Springer, 100--116.
[26]
W. Jamroga, M. Knapik, D. Kurpiewski, and ?. Mikulski. 2019. Approximate Verification of Strategic Abilities under Imperfect Information. Artificial Intelligence 277 (2019).
[27]
Wojciech Jamroga, Beata Konikowska, Wojciech Penczek, and Damian Kurpiewski. 2020. Multi-valued Verification of Strategic Ability. Fundamenta Informaticae1 75, 1--4 (2020), 207--251. https://doi.org/10.3233/FI-2020--1955
[28]
Wojciech Jamroga, Damian Kurpiewski, and Vadim Malvone. 2020. Natural Strategic Abilities in Voting Protocols. CoRRabs/2007.12424 (2020). arXiv:2007.12424 https://arxiv.org/abs/2007.12424
[29]
W. Jamroga, W. Penczek, P. Dembi'ski, and A. Mazurkiewicz. 2018. Towards Partial Order Reductions for Strategic Ability. In Proceedings of the 17th Inter-national Conference on Autonomous Agents and Multiagent Systems (AAMAS). IFAAMAS, 156--165.
[30]
W. Jamroga, W. Penczek, and T. Sidoruk. 2020. Strategic Abilities of Asynchronous Agents: Semantic Paradoxes and How to Tame Them. CoRRabs/2003.03867(2020). arXiv:2003.03867[cs.LO]https://arxiv.org/abs/2003.03867
[31]
W. Jamroga, W. Penczek, T. Sidoruk, P. Dembi'ski, and A. Mazurkiewicz. 2020. Towards Partial Order Reductions for Strategic Ability. Journal of Artificial Intelligence Research 68 (2020), 817--850. https://doi.org/10.1613/jair.1.11936
[32]
M. Kacprzak and W. Penczek. 2004. Unbounded Model Checking for Alternating-Time Temporal Logic. In Proceedings of International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS). IEEE Computer Society,646--653. https://doi.org/10.1109/AAMAS.2004.10089
[33]
D. Kurpiewski, W. Jamroga, and M. Knapik. 2019. STV: Model Checking for Strategies under Imperfect Information. In Proceedings of the 18th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2019. IFAA-MAS, 2372--2374.
[34]
Damian Kurpiewski, Michal Knapik, and Wojciech Jamroga. 2019. On Domination and Control in Strategic Ability. In Proceedings of the 18th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2019. IFAA-MAS, 197--205.
[35]
A. Lomuscio, W. Penczek, and H. Qu. 2010. Partial Order Reductions for Model Checking Temporal-epistemic Logics over Interleaved Multi-agent Systems. Fundamenta Informaticae 101, 1--2 (2010), 71--90. https://doi.org/10.3233/FI-2010--276
[36]
Alessio Lomuscio, Wojciech Penczek, and Hongyang Qu. 2010. Partial order reductions for model checking temporal epistemic logics over interleaved multi-agent systems. In 9th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2010), Toronto, Canada, May 10--14, 2010, Volume 1--3. IFAAMAS, 659--666.
[37]
A. Lomuscio, H. Qu, and F. Raimondi. 2017. MCMAS: An Open-Source Model Checker for the Verification of Multi-Agent Systems. International Journal on Software Tools for Technology Transfer19, 1 (2017), 9--30. https://doi.org/10.1007/s10009-015-0378-x
[38]
A. Lomuscio and F. Raimondi. 2006. MCMAS : A Model Checker for Multi-Agent Systems. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems (TACAS) (Lecture Notes in Computer Science, Vol. 4314). Springer, 450--454.
[39]
Doron A. Peled. 1993. All from One, One for All: on Model Checking Using Representatives. In Proceedings of CAV (Lecture Notes in Computer Science, Vol. 697), Costas Courcoubetis (Ed.). Springer, 409--423. https://doi.org/10.1007/3--540--56922--7_34
[40]
J. Pilecki, M.A. Bednarczyk, and W. Jamroga. 2014. Synthesis and Verification of Uniform Strategies for Multi-Agent Systems. In Proceedings of CLIMA XV (Lecture Notes in Computer Science, Vol. 8624). Springer, 166--182.
[41]
J. Pilecki, M.A. Bednarczyk, and W. Jamroga. 2017. SMC: Synthesis of Uniform Strategies and Verification of Strategic Ability for Multi-Agent Systems. Journal of Logic and Computation 27, 7 (2017), 1871--1895.https://doi.org/10.1093/logcom/exw032
[42]
P.Y.A. Ryan. 2010. The Computer Ate My Vote. In Formal Methods: State of the Art and New Directions. Springer, 147--184.
[43]
P. Y. Schobbens. 2004. Alternating-Time Logic with Imperfect Recall. Electronic Notes in Theoretical Computer Science 85, 2 (2004), 82--93.
[44]
M. Tabatabaei, W. Jamroga, and Peter Y. A. Ryan. 2016. 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. ACM, 1:1--1:8. https://doi.org/10.1145/2970030.2970039
[45]
W. van der Hoek and M. Wooldridge. 2002. Tractable Multiagent Planning for Epistemic Goals. In Proceedings of the First International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS-02), C. Castelfranchi and W.L. Johnson (Eds.). ACM Press, New York, 1167--1174.
Index Terms
- STV+Reductions: Towards Practical Verification of Strategic Ability Using Model Reductions
Recommendations
Towards Assume-Guarantee Verification of Strategic Ability
AAMAS '22: Proceedings of the 21st International Conference on Autonomous Agents and Multiagent SystemsFormal verification of strategic abilities is a hard problem. We propose to use the methodology of assume-guarantee reasoning in order to facilitate model checking of alternating-time temporal logic with imperfect information and imperfect recall.
Towards Partial Order Reductions for Strategic Ability
AAMAS '18: Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent SystemsWe propose a general semantics for strategic abilities of agents in asynchronous systems, with and without perfect information. Based on the semantics, we show some general complexity results for verification of strategic abilities in asynchronous ...
Verification of Multi-Agent Systems via Predicate Abstraction against ATLK Specifications
AAMAS '16: Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent SystemsWe present a predicate abstraction technique for the verification of multi-agent systems against specifications defined in the epistemic logic ATLK, interpreted on a three-valued semantics. We reduce an infinite-state multi-agent program to a finite ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
May 2021
1899 pages
ISBN:9781450383073
- General Chairs:
- Frank Dignum,
- Alessio Lomuscio,
- Program Chairs:
- Ulle Endriss,
- Ann Nowé
Sponsors
Publisher
International Foundation for Autonomous Agents and Multiagent Systems
Richland, SC
Publication History
Published: 03 May 2021
Check for updates
Author Tags
Qualifiers
- Demonstration
Funding Sources
- Luxembourg National Research Fund (FNR) and the National Centre for Research and Development (NCBiR) Poland
Conference
AAMAS '21
Sponsor:
AAMAS '21: 20th International Conference on Autonomous Agents and Multiagent Systems
May 3 - 7, 2021
Virtual Event, United Kingdom
Acceptance Rates
Overall Acceptance Rate 1,155 of 5,036 submissions, 23%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 13Total Downloads
- Downloads (Last 12 months)1
- Downloads (Last 6 weeks)0
Reflects downloads up to 19 Nov 2024
Other Metrics
Citations
Cited By
View all- Briola DFerrando AMascardi V(2023)Fantastic MASs and Where to Find Them: First Results and Lesson LearnedEngineering Multi-Agent Systems10.1007/978-3-031-48539-8_16(233-252)Online publication date: 29-May-2023
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in