Document Open Access Logo

Model Checking Strategic Ability - Why, What, and Especially: How? (Invited Paper)

Author Wojciech Jamroga

PDF

File

Thumbnail PDF
PDF
LIPIcs.TIME.2018.3.pdf
  • Filesize: 0.75 MB
  • 10 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Computing methodologies → Multi-agent systems
Keywords
  • model checking
  • strategic ability
  • alternating-time temporal logic
  • imperfect information games
  • approximate verification
  • model reductions

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Automated verification of discrete-state systems has been a hot topic in computer science for over 35 years. Model checking of temporal and strategic properties is one of the most prominent and most successful approaches here. In this talk, I present a brief introduction to the topic, and mention some relevant properties that one might like to verify this way. Then, I describe some recent results on approximate model checking and model reductions, which can be applied to facilitate verification of notoriously hard cases.

Cite As Get BibTex

Wojciech Jamroga. Model Checking Strategic Ability - Why, What, and Especially: How? (Invited Paper). In 25th International Symposium on Temporal Representation and Reasoning (TIME 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 120, pp. 3:1-3:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.TIME.2018.3

Author Details

Wojciech Jamroga
  • Institute of Computer Science, Polish Academy of Sciences, Warsaw, Poland

Funding

  • Jamroga, Wojciech: The author acknowledges the support of the National Centre for Research and Development (NCBR), Poland, under the PolLux project VoteVerif (POLLUX-IV/1/2016).

References

  1. T. Ågotnes, V. Goranko, W. Jamroga, and M. Wooldridge. Knowledge and ability. In H.P. van Ditmarsch, J.Y. Halpern, W. van der Hoek, and B.P. Kooi, editors, Handbook of Epistemic Logic, pages 543-589. College Publications, 2015. Google Scholar
  2. R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time Temporal Logic. Journal of the ACM, 49:672-713, 2002. URL: http://dx.doi.org/10.1145/585265.585270.
  3. F. Belardinelli, R. Condurache, C. Dima, W. Jamroga, and A.V. Jones. Bisimulations for verification of strategic abilities with application to ThreeBallot voting protocol. In Proceedings of the 16th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2017, pages 1286-1295. IFAAMAS, 2017. Google Scholar
  4. 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. Google Scholar
  5. N. Bulling, V. Goranko, and W. Jamroga. Logics for reasoning about strategic abilities in multi-player games. In J. van Benthem, S. Ghosh, and R. Verbrugge, editors, Models of Strategic Reasoning. Logics, Games, and Communities, volume 8972 of Lecture Notes in Computer Science, pages 93-136. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-48540-8.
  6. N. Bulling and W. Jamroga. Alternating epistemic mu-calculus. In Proceedings of IJCAI-11, pages 109-114, 2011. Google Scholar
  7. S. Busard. Symbolic Model Checking of Multi-Modal Logics: Uniform Strategies and Rich Explanations. PhD thesis, Universite Catholique de Louvain, 2017. Google Scholar
  8. 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. URL: http://dx.doi.org/10.1007/978-3-319-11737-9_3.
  9. S. Busard, C. Pecheur, H. Qu, and F. Raimondi. Reasoning about memoryless strategies under partial observability and unconditional fairness constraints. Information and Computation, 242:128-156, 2015. URL: http://dx.doi.org/10.1016/j.ic.2015.03.014.
  10. E.M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999. Google Scholar
  11. C. Dima, B. Maubert, and S. Pinchinat. The expressive power of epistemic μ-calculus. CoRR, abs/1407.5166, 2014. Google Scholar
  12. C. Dima, B. Maubert, and S. Pinchinat. Relating paths in transition systems: The fall of the modal mu-calculus. In Proceedings of Mathematical Foundations of Computer Science (MFCS), volume 9234 of Lecture Notes in Computer Science, pages 179-191. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-48057-1_14.
  13. C. Dima and F.L. Tiplea. Model-checking ATL under imperfect information and perfect recall semantics is undecidable. CoRR, abs/1102.4225, 2011. Google Scholar
  14. D.P. Guelev, C. Dima, and C. Enea. 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. Google Scholar
  15. 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. Google Scholar
  16. W. Jamroga, M. Knapik, and D. Kurpiewski. Fixpoint approximation of strategic abilities under imperfect information. In Proceedings of the 16th International Conference on Autonomous Agents and Multiagent Systems (AAMAS), pages 1241-1249. IFAAMAS, 2017. Google Scholar
  17. 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), Lecture Notes in Computer Science. Springer, 2018. To appear. Google Scholar
  18. W. Jamroga, M. Knapik, D. Kurpiewski, and Łukasz Mikulski. Approximate verification of strategic abilities under imperfect information. Artificial Intelligence, 2018. To appear. Google Scholar
  19. 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. Google Scholar
  20. 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, 2015. Availabe online. URL: http://dx.doi.org/10.1007/s10009-015-0378-x.
  21. J. Pilecki, M.A. Bednarczyk, and W. Jamroga. Synthesis and verification of uniform strategies for multi-agent systems. In Proceedings of CLIMA XV, volume 8624 of Lecture Notes in Computer Science, pages 166-182. Springer, 2014. Google Scholar
  22. P. Y. Schobbens. Alternating-time logic with imperfect recall. Electronic Notes in Theoretical Computer Science, 85(2):82-93, 2004. Google Scholar
  23. M. Tabatabaei, W. Jamroga, and Peter 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. URL: http://dx.doi.org/10.1145/2970030.2970039.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact