Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Rational Capability in Concurrent Games

Yinfeng Li, Emiliano Lorini, Munyque Mittelmann

TL;DR

This work extends concurrent game structures by equipping agents with per-state preferences over computations and introduces two logics, $\textsf{R-ATL}$ and $\textsf{R-CL}$, that reason about a coalition's rational capabilities under a minimal dominance-based notion of rationality. It establishes a tree-like model property for $\textsf{R-ATL}$, and shows polynomial embeddings into $\mathsf{ATL}$ and $\mathsf{CL}$ under stable preferences (with extensions without stability for certain cases), yielding tight satisfiability complexities. It also provides a sound and complete axiomatization for $\textsf{R-CL}$ and a polynomial-time model-checking algorithm for $\textsf{R-ATL}$ on GCSPs with short-sighted preferences, making rational capability reasoning tractable in restricted settings. Overall, the framework integrates explicit agent preferences into CGS semantics to analyze rational capabilities, offering formal tools and complexity results for reasoning about agents' rational strategies and obligations.

Abstract

We extend concurrent game structures (CGSs) with a simple notion of preference over computations and define a minimal notion of rationality for agents based on the concept of dominance. We use this notion to interpret a CL and an ATL languages that extend the basic CL and ATL languages with modalities for rational capability, namely, a coalition's capability to rationally enforce a given property. For each of these languages, we provide results about the complexity of satisfiability checking and model checking as well as about axiomatization.

Rational Capability in Concurrent Games

TL;DR

This work extends concurrent game structures by equipping agents with per-state preferences over computations and introduces two logics, and , that reason about a coalition's rational capabilities under a minimal dominance-based notion of rationality. It establishes a tree-like model property for , and shows polynomial embeddings into and under stable preferences (with extensions without stability for certain cases), yielding tight satisfiability complexities. It also provides a sound and complete axiomatization for and a polynomial-time model-checking algorithm for on GCSPs with short-sighted preferences, making rational capability reasoning tractable in restricted settings. Overall, the framework integrates explicit agent preferences into CGS semantics to analyze rational capabilities, offering formal tools and complexity results for reasoning about agents' rational strategies and obligations.

Abstract

We extend concurrent game structures (CGSs) with a simple notion of preference over computations and define a minimal notion of rationality for agents based on the concept of dominance. We use this notion to interpret a CL and an ATL languages that extend the basic CL and ATL languages with modalities for rational capability, namely, a coalition's capability to rationally enforce a given property. For each of these languages, we provide results about the complexity of satisfiability checking and model checking as well as about axiomatization.

Paper Structure

This paper contains 22 sections, 11 theorems, 18 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Related work
  3. Semantics
  4. Preliminaries
  5. Adding preferences
  6. Language
  7. Tree-like model property and embedding
  8. Tree-like model property
  9. Embedding
  10. Axiomatization for $\textsf{R-CL} \xspace$
  11. Model checking
  12. Conclusion
  13. Proof of Lemma \ref{['lemmacrucial']}
  14. Proof of Theorem \ref{['theo:embedding']}
  15. A counter-model
  16. ...and 7 more sections

Key Result

Lemma 1

Let $\varphi \in \mathcal{L}_{\textsf{R-ATL} \xspace}(\mathbb{P}, \mathbb{AGT} )$. Then,

Figures (2)

  • Figure 1: Model $M_{cross}$ representing a system with two vehicles approaching an intersection. Arrows represent transitions between states and are labeled by joint actions of $v_1$ and $v_2$. $(*,*)$ denotes any action.
  • Figure 2: Representation of the unravelling of $M_{cross}$ from the initial state ($w_0$). Branches represent (groups of) computations. Transitions are labeled by the action taken by $v_1$ and $*$ denotes any action. Self-loops indicate computations where the state is repeated. Grey states indicate computations with an infinite suffix that repeats on the same state. Labels in the form under the grey states represent the preference relations $\preceq_{v_1,w_0}$ and $\preceq_{v_2,w_0}$ of the agents $v_1$ and $v_2$, respectively. Computations labeled with $+_i$ are strictly preferred to $=_i$ by agent $v_i$, and $=_i$ are strictly preferred to $-_i$ by agent $v_i$ (where $i = \{1,2\}$).

Theorems & Definitions (29)

  • Definition 1: CGS
  • Example 1: Crossing road
  • Definition 2: Path and computation
  • Definition 3: Individual strategy
  • Definition 4: Collective strategy
  • Definition 5: Generated computations
  • Definition 6: CGS with preferences
  • Example 2: Crossing road (cont.)
  • Definition 7: Dominated strategies
  • Example 3: Crossing road (cont.)
  • ...and 19 more