Verification of Robust Multi-Agent Systems

TL;DR

The paper tackles verifying robust strategies for stochastic multi-agent systems with imperfect information when transition probabilities are uncertain. It introduces observation-based, bounded-memory strategies represented by finite automata and defines three robustness notions: $\varepsilon$-perturbations and parametric uncertainties with both fixed and unbounded parameter counts, within a $\mathsf{PATL}$ framework. It provides a spectrum of complexity results, ranging from polynomial-time reachability checks under $\varepsilon$-perturbations to $\mathbf{NP}\cap\mathbf{co}$-$\mathbf{NP}$ and $\forall\mathbb{R}$/$\Sigma_3^{\mathbb{R}}$ classifications for parametric models, and demonstrates how automata-based strategies offer expressive power without inflating worst-case costs. The work also connects robust MAS verification to interval and parametric MDPs, discusses practical cyber-physical applications, and outlines future directions for computing strategy robustness and lower bounds. Overall, it establishes decidability and actionable complexity bounds for robust, memory-bounded strategic verification in uncertain, multi-agent, partially observable environments.

Abstract

Stochastic multi-agent systems are a central modeling framework for autonomous controllers, communication protocols, and cyber-physical infrastructures. In many such systems, however, transition probabilities are only estimated from data and may therefore be partially unknown or subject to perturbations. In this paper, we study the verification of robust strategies in stochastic multi-agent systems with imperfect information, in which coalitions must satisfy a temporal specification while dealing with uncertain system transitions, partial observation, and adversarial agents. By focusing on bounded-memory strategies, we introduce a robust variant of the model-checking problem for a probabilistic, observation-based extension of Alternating-time Temporal Logic. We characterize the complexity of this problem under different notions of perturbation, thereby clarifying the computational cost of robustness in stochastic multi-agent verification and supporting the use of bounded-memory strategies in uncertain environments.

Figures (5)

• Figure 1: System $\mathcal{}$CGS$\xspace_{river}$ representing the interaction between two companies. The transition function is written in terms of labels on the arrows. Each transition from state $q$ to $q'$ is annotated with one or more labels of the form $(x, y)/z$ where $(x, y)$ denote the joint action of the companies in state $q$, and z denotes the probability of arriving at the state $q'$. The transition probabilities for the joint action $(d,t)$ are the same as for $(t,d)$, and are thus omitted.
• Figure 2: An MDP $\mathcal{G}_g$ where scheduler-based strategies are more general than sequential strategies.
• Figure 3: A two-state scheduler enforcing $\varphi_g$ on $\mathcal{G}_g$.
• Figure 4: The parametric system $\mathcal{}$CGS$\xspace^p_{river}$ shows the case where we are unsure of some transitions, that may change together depending on $x\in[0,0.25]$.
• Figure 5: The system $\mathcal{}$CGS$\xspace_{river}'$, obtained from a realisability of the $0.05$-approximated system $\mathcal{}$CGS$\xspace_{0.05, river}$.

Theorems & Definitions (28)

• definition 1: General Bounded-Memory Strategies.
• proposition 1
• Remark 1
• definition 2
• definition 3
• Remark 2
• definition 4
• proposition 2: From DBLP:conf/prima/HaoSLSGDL12
• Remark 3
• definition 5