Parameterised Verification of Strategic Properties in Probabilistic Multi-Agent Systems


We present a framework for verifying strategic behaviour in an unbounded multi-agent system. We introduce a novel probabilistic semantics for parameterised multi-agent systems and define the corresponding verification problem against two probabilistic variants of alternating-time temporal logic. We define a verification procedure using an abstract model construction. We show that the procedure is complete for one variant of our specification language, and partial for the other. We present an implementation and report experimental results.

Proceedings of the 19th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2020)