Research map / Multi-agent systems and games / Games and equilibria
Abstraction of Situation Calculus Concurrent Game Structures
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Extends situation-calculus agent abstraction to multi-agent synchronous games (SCSGSs), defining sound/complete m-bisimulation-based abstraction and showing that µATL-FO properties verified at the abstract level transfer to the concrete level.
Problem
Verifying strategic properties of multi-agent synchronous games with first-order state is costly on concrete models; abstraction must preserve strategic (µATL-FO) properties while agents act concurrently.
Approach
Generalizes the BDL17 situation-calculus abstraction framework to synchronous concurrent games: a single tick action with joint moves, a refinement mapping implementing abstract moves as move-based Golog programs synchronized via sync, and constraints (proper refinement, agents can always execute abstract moves to completion) that let µATL-FO properties transfer from abstract to concrete models.
Key results
- Proves that the repair-shop abstraction SCSGS is a sound and complete abstraction of the concrete SCSGS under the refinement mapping (Proposition 2).
- Proves Theorem 11: if a mu-ATL-FO property holds at the abstract level and constraints 4, 6, 8 hold, the mapped property holds at the concrete level.
- Shows the example properties <<{Disp,RR1}>>F exists i Repaired(i) and a repair-shop liveness property hold at the abstract level and therefore transfer to the concrete level.
Limitations
- Requires the assumption that agents can always execute abstract moves to completion even without controlling their outcomes (Constraint 4).
- Purely theoretical; no implementation or empirical evaluation.
- Reasoning in the first-order situation calculus is undecidable in general.
Experimental setup
Builds on: Banihashemi, De Giacomo, and Lesperance 2017 (BDL17) agent abstraction De Giacomo, Lesperance, and Pearce 2016 SCSGS and move-based Golog mu-ATL ConGolog
Closest papers by meaning
- Abstraction in Situation Calculus Action Theories (AAAI 2017 · similarity 0.90)
- A Syntactic Approach to Computing Complete and Sound Abstraction in the Situation Calculus (AAAI 2025 · similarity 0.89)
- LTLf Synthesis on First-Order Agent Programs in Nondeterministic Environments (AAAI 2025 · similarity 0.87)
- Situation Calculus Temporally Lifted Abstractions for Generalized Planning (AAAI 2025 · similarity 0.85)
- On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing (AAAI 2024 · similarity 0.84)
- Approximate State Abstraction for Markov Games (AAAI 2025 · similarity 0.84)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.