Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Strategic Abilities of Asynchronous Agents: Semantic Side Effects and How to Tame Them

Wojciech Jamroga, Wojciech Penczek, Teofil Sidoruk

TL;DR

This work proposes how to avoid the problems by a suitable extension of the representations and change of the execution semantics for asynchronous MAS, and proves that the model reduction scheme still works in the modified framework.

Abstract

Recently, we have proposed a framework for verification of agents' abilities in asynchronous multi-agent systems, together with an algorithm for automated reduction of models. The semantics was built on the modeling tradition of distributed systems. As we show here, this can sometimes lead to counterintuitive interpretation of formulas when reasoning about the outcome of strategies. First, the semantics disregards finite paths, and thus yields unnatural evaluation of strategies with deadlocks. Secondly, the semantic representations do not allow to capture the asymmetry between proactive agents and the recipients of their choices. We propose how to avoid the problems by a suitable extension of the representations and change of the execution semantics for asynchronous MAS. We also prove that the model reduction scheme still works in the modified framework.

Strategic Abilities of Asynchronous Agents: Semantic Side Effects and How to Tame Them

TL;DR

This work proposes how to avoid the problems by a suitable extension of the representations and change of the execution semantics for asynchronous MAS, and proves that the model reduction scheme still works in the modified framework.

Abstract

Recently, we have proposed a framework for verification of agents' abilities in asynchronous multi-agent systems, together with an algorithm for automated reduction of models. The semantics was built on the modeling tradition of distributed systems. As we show here, this can sometimes lead to counterintuitive interpretation of formulas when reasoning about the outcome of strategies. First, the semantics disregards finite paths, and thus yields unnatural evaluation of strategies with deadlocks. Secondly, the semantic representations do not allow to capture the asymmetry between proactive agents and the recipients of their choices. We propose how to avoid the problems by a suitable extension of the representations and change of the execution semantics for asynchronous MAS. We also prove that the model reduction scheme still works in the modified framework.

Paper Structure

This paper contains 28 sections, 14 theorems, 1 equation, 5 figures.

Table of Contents

  1. Introduction
  2. Models of Multi-agent Systems
  3. Asynchronous Multi-agent Systems
  4. Interleaved Interpreted Systems
  5. Reasoning About Abilities: ATL*
  6. Syntax
  7. Strategies and Outcomes
  8. Strategic Ability for Asynchronous Systems
  9. Semantic Problems and How to Avoid Them
  10. Deadlock Strategies and Finite Paths
  11. Solution: Adding Silent Transitions
  12. Playing Against Reactive Opponents
  13. Opponent-Reactiveness
  14. Encoding Strategic Deadlock-Freeness Under Opponent-Reactiveness in AMAS
  15. Concurrency-Fairness Revisited
  16. ...and 13 more sections

Key Result

Proposition 4.4

For any AMAS $S\xspace$, any state $g\in IIS^{\text{\normalsize$\epsilon$}}(S\xspace)$, and any strategy $\sigma_A$, we have that $enabled_{IIS^{\text{\normalsize$\epsilon$}}(S\xspace)}(g,\sigma_A(state)) \neq \emptyset$.

Figures (5)

  • Figure 1: Simple asynchronous MAS: agents $gc$, $oc$, and $sc$. A joint strategy of agents $\{{gc,oc}\}$ is highlighted.
  • Figure 2: Model $M_\mathit{conf}$ for the conference scenario. We highlight the transitions enabled by the strategy in Figure \ref{['fig:conference-strategy']}, and the resulting reachable states.
  • Figure 3: Casting a ballot: voter $v$ (left) and EBM $ebm$ (right)
  • Figure 4: Undeadlocked IIS for the voting scenario
  • Figure 5: The auxiliary agent added in $S\xspace^{\text{\normalsize$\epsilon$}}$

Theorems & Definitions (50)

  • Definition 2.1: Asynchronous MAS
  • Example 2.2: Conference in times of epidemic
  • Definition 2.3: Model
  • Example 2.4: Conference
  • Example 3.1: Conference
  • Example 3.2: Conference
  • Definition 3.3: Enabled events
  • Example 3.4: Conference
  • Definition 3.5: Outcome paths
  • Definition 3.6: CF-outcome
  • ...and 40 more