Abstraction of Situation Calculus Concurrent Game Structures
Yves Lesperance, Giuseppe De Giacomo, Maryam Rostamigiv, Shakil M. Khan
Abstract
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 mu-calculus mu-ATL-FO. We show that we can exploit abstraction in verifying mu-ATL-FO properties of SCSGSs under the assumption that agents can always execute abstract moves to completion even if not fully controlling their outcomes.
BibTeX
@article{Lesperance_De Giacomo_Rostamigiv_Khan_2024, title={Abstraction of Situation Calculus Concurrent Game Structures}, volume={38}, url={https://ojs.aaai.org/index.php/AAAI/article/view/28933}, DOI={10.1609/aaai.v38i9.28933}, abstractNote={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 mu-calculus mu-ATL-FO. We show that we can exploit abstraction in verifying mu-ATL-FO properties of SCSGSs under the assumption that agents can always execute abstract moves to completion even if not fully controlling their outcomes.}, number={9}, journal={Proceedings of the AAAI Conference on Artificial Intelligence}, author={Lesperance, Yves and De Giacomo, Giuseppe and Rostamigiv, Maryam and Khan, Shakil M.}, year={2024}, month={Mar.}, pages={10624-10634} }