Towards Assume-Guarantee Verification of Abilities in Stochastic Multi-Agent Systems

TL;DR

This paper advances the verification of multi-agent systems with stochastic behaviors by proposing assume-guarantee schemes for probabilistic logic, enabling scalable analysis of agents with imperfect information.

Contribution

It introduces new assume-guarantee verification schemes for probabilistic ATL with imperfect information and a novel variant of alternating-time logic for strategic reasoning.

Findings

Proved the soundness of the proposed verification schemes

Discussed the completeness of the schemes

Introduced a new variant of alternating-time logic

Abstract

Model checking of strategic abilities is a notoriously hard problem, even more so in the realistic case of agents with imperfect information, acting in a stochastic environment. Assume-guarantee reasoning can be of great help here, providing a way to decompose the complex problem into a small set of easier subproblems. In this paper, we propose several schemes for assume-guarantee verification of probabilistic alternating-time temporal logic with imperfect information. We prove the soundness of the schemes, and discuss their completeness. On the way, we also propose a new variant of (non-probabilistic) alternating-time logic, where the strategic modalities capture "achieving at most $\varphi$," analogous to Levesque's logic of "only knowing."