Abstraction of Situation Calculus Concurrent Game Structures

Authors: Yves Lesperance, Giuseppe De Giacomo, Maryam Rostamigiv, Shakil M. Khan

AAAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Theoretical We present a general framework for abstracting agent behavior in multi-agent synchronous games in the situation calculus, which provides a first-order representation of the state and allows us to model how plays depend on the data and objects involved. We represent such games as action theories of a special form called situation calculus synchronous game structures (SCSGSs), in which we have a single action tick whose effects depend on the combination of moves selected by the players. In our framework, one specifies both an abstract SCSGS and a concrete SCSGS, as well as a refinement mapping that specifies how each abstract move is implemented by a Golog program defined over the concrete SCSGS. We define notions of sound and complete abstraction with respect to a mapping over such SCSGS. To express strategic properties on the abstract and concrete games we adopt a first-order variant of alternating-time µ-calculus µATL-FO. We show that we can exploit abstraction in verifying µATL-FO properties of SCSGSs under the assumption that agents can always execute abstract moves to completion even if not fully controlling their outcomes.
Researcher Affiliation Academia Yves Lesp erance1, Giuseppe De Giacomo2, Maryam Rostamigiv3, Shakil M. Khan3 1York University, Toronto, ON, Canada 2University of Oxford, Oxford, UK 3University of Regina, Regina, SK, Canada lesperan@eecs.yorku.ca, giuseppe.degiacomo@cs.ox.ac.uk, maryam.rostamigiv@uregina.ca, shakil.khan@uregina.ca
Pseudocode No The paper describes the syntax and semantics of Golog programs using formal logical expressions and predicates (e.g., Trans, Final, Do), but does not present pseudocode in a dedicated block or figure.
Open Source Code No The paper does not provide any concrete access to source code for the methodology described.
Open Datasets No The paper is theoretical and does not involve empirical studies with datasets. Examples are used for illustration, not data evaluation.
Dataset Splits No The paper is theoretical and does not involve empirical studies with dataset splits. Examples are used for illustration, not data evaluation.
Hardware Specification No The paper is theoretical and does not describe any specific hardware used for experiments.
Software Dependencies No The paper does not provide specific ancillary software details with version numbers.
Experiment Setup No The paper is theoretical and does not describe an experimental setup with hyperparameters or system-level training settings.