KR2024Proceedings of the 21st International Conference on Principles of Knowledge Representation and ReasoningProceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning

Hanoi, Vietnam. November 2-8, 2024.

Edited by

ISSN: 2334-1033
ISBN: 978-1-956792-05-8

Sponsored by
Published by

Copyright © 2024 International Joint Conferences on Artificial Intelligence Organization

Verification of General Games with Imperfect Information Using Strategy Logic

  1. Yifan He(University of New South Wales)
  2. Munyque Mittelmann(University of Naples Federico II)
  3. Aniello Murano(University of Naples Federico II)
  4. Abdallah Saffidine(University of New South Wales)
  5. Michael Thielscher(University of New South Wales)

Keywords

  1. Reasoning about actions and change, action languages-General
  2. Reasoning about knowledge, beliefs, and other mental attitudes-General
  3. Reasoning in multi-agent systems-General

Abstract

The Game Description Language with Imperfect Information (GDL-II) is a lightweight formalism for representing the rules of arbitrary games, including those where players have private information. Its purpose is to build general game-playing systems, that is, automated players that can understand the rules of games and learn how to play them without human intervention. Epistemic Strategy Logic (SLK), on the other hand, is a rich logical framework for reasoning about multi-agent systems and the strategic behavior of agents with partial observability. To enable a general game-playing system to take advantage of this rich formalism for the automatic verification of properties of games, we present a formal translation from GDL-II to SLK models. We prove the correctness of this translation and show how crucial properties of general games, including playability and the existence of Nash equilibria, can be expressed as formulas in SLK. Finally, we demonstrate the application of an existing model-checking system for SLK to verify the properties of GDL-II games.