Can agents rationally enforce properties in concurrent games?
Rational Capability in Concurrent Games
This paper extends Concurrent Game Structures (CGSs) with preferences to model rational agent behavior. It introduces two new logics, R-ATL and R-CL, which augment the existing Alternating-time Temporal Logic (ATL) and Coalition Logic (CL) with operators for rational strategic capability. These new operators evaluate whether a group of agents can achieve a goal by using strategies where no individual agent's strategy is dominated by another, regardless of what other agents do (strong dominance). The paper establishes complexity results for these logics and provides a complete axiomatization for R-CL, as well as a model-checking algorithm for R-ATL with a specific type of preference.
For LLM-based multi-agent systems, this research offers a formal framework to reason about and verify the behavior of agents with explicit preferences. The concept of rational capability is particularly relevant, as it allows developers to check whether agents will reliably make rational choices when interacting, especially crucial when relying on LLMs where outputs can be unpredictable. The complexity results and algorithms presented provide tools for analyzing and verifying these systems, laying a groundwork for building more robust and predictable multi-agent applications.