Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Natural Strategic Ability in Stochastic Multi-Agent Systems

Raphaël Berthon, Joost-Pieter Katoen, Munyque Mittelmann, Aniello Murano

TL;DR

The paper extends probabilistic temporal logics to stochastic multi-agent systems by introducing NatPATL and NatPATL*, which restrict strategies to natural, memory-bounded plans. It provides a comprehensive complexity landscape: NatPATL with deterministic strategies is NP-complete, NatPATL* with deterministic strategies is 2NEXPTIME, and unrestricted variants lie in EXPSPACE and 3EXPSPACE, respectively, with probabilistic strategies increasing these bounds to EXPSPACE/3EXPSPACE. The authors formalize behavioral natural strategies, define probability spaces over outcomes, and illustrate the framework with motivating examples on voting and access control. They also compare expressivity and distinguishing power with classical PATL/PATL*, showing that natural strategies capture properties beyond combinatorial strategies and vice versa, underlining both practical relevance and theoretical richness. The results point to a favorable balance between expressivity and model-checking complexity for real-world MAS verification and suggest future work on extensions and optimization.

Abstract

Strategies synthesized using formal methods can be complex and often require infinite memory, which does not correspond to the expected behavior when trying to model Multi-Agent Systems (MAS). To capture such behaviors, natural strategies are a recently proposed framework striking a balance between the ability of agents to strategize with memory and the model-checking complexity, but until now has been restricted to fully deterministic settings. For the first time, we consider the probabilistic temporal logics PATL and PATL* under natural strategies (NatPATL and NatPATL*, resp.). As main result we show that, in stochastic MAS, NatPATL model-checking is NP-complete when the active coalition is restricted to deterministic strategies. We also give a 2NEXPTIME complexity result for NatPATL* with the same restriction. In the unrestricted case, we give an EXPSPACE complexity for NatPATL and 3EXPSPACE complexity for NatPATL*.

Natural Strategic Ability in Stochastic Multi-Agent Systems

TL;DR

The paper extends probabilistic temporal logics to stochastic multi-agent systems by introducing NatPATL and NatPATL*, which restrict strategies to natural, memory-bounded plans. It provides a comprehensive complexity landscape: NatPATL with deterministic strategies is NP-complete, NatPATL* with deterministic strategies is 2NEXPTIME, and unrestricted variants lie in EXPSPACE and 3EXPSPACE, respectively, with probabilistic strategies increasing these bounds to EXPSPACE/3EXPSPACE. The authors formalize behavioral natural strategies, define probability spaces over outcomes, and illustrate the framework with motivating examples on voting and access control. They also compare expressivity and distinguishing power with classical PATL/PATL*, showing that natural strategies capture properties beyond combinatorial strategies and vice versa, underlining both practical relevance and theoretical richness. The results point to a favorable balance between expressivity and model-checking complexity for real-world MAS verification and suggest future work on extensions and optimization.

Abstract

Strategies synthesized using formal methods can be complex and often require infinite memory, which does not correspond to the expected behavior when trying to model Multi-Agent Systems (MAS). To capture such behaviors, natural strategies are a recently proposed framework striking a balance between the ability of agents to strategize with memory and the model-checking complexity, but until now has been restricted to fully deterministic settings. For the first time, we consider the probabilistic temporal logics PATL and PATL* under natural strategies (NatPATL and NatPATL*, resp.). As main result we show that, in stochastic MAS, NatPATL model-checking is NP-complete when the active coalition is restricted to deterministic strategies. We also give a 2NEXPTIME complexity result for NatPATL* with the same restriction. In the unrestricted case, we give an EXPSPACE complexity for NatPATL and 3EXPSPACE complexity for NatPATL*.
Paper Structure (16 sections, 9 theorems, 15 equations, 1 figure, 1 table)

This paper contains 16 sections, 9 theorems, 15 equations, 1 figure, 1 table.

Table of Contents

  1. Introduction
  2. Contribution.
  3. Outline.
  4. Related Work
  5. Preliminaries
  6. Behavioral Natural Strategies
  7. Complexity of Natural Strategies.
  8. Relation to Game Theory.
  9. $\mathsf{PATL_{\mathrm{}}}$ and $\mathsf{PATL_\mathrm{}^*}$ with Natural Strategies
  10. Probability Space on Outcomes.
  11. Motivating Examples
  12. Model Checking Complexity
  13. Expressivity
  14. Conclusion
  15. Acknowledgements
  16. ...and 1 more sections

Key Result

Theorem 1

Model checking Nat$\mathsf{PATL_{\mathrm{r}}}$ (respectively Nat$\mathsf{PATL_{\mathrm{R}}}$) with deterministic natural strategies for the coalition is in $\Delta_2^P = \mathbf{{P}}\xspace^{\mathbf{{NP}}\xspace}$.

Figures (1)

  • Figure 1: A robot in a maze, where $=$ and $\times$ denote a door respectively controlled by the coalition or the agents not in the coalition. Full lines represent walls. $t_0,t_1$ are two targets.

Theorems & Definitions (30)

  • Example 1: Secure voting
  • Example 2: Secure voting, continued
  • Definition 1
  • Definition 2: Nat$\mathsf{PATL_{\mathrm{}}}$ syntax
  • Definition 3: Nat$\mathsf{PATL_{\mathrm{}}}$ and Nat$\mathsf{PATL_\mathrm{}^*}$ semantics
  • Example 3: Access control
  • Example 4: Secure voting, continued
  • Definition 4
  • Definition 5: Number of negations
  • Theorem 1
  • ...and 20 more