Multi-Agent Verification and Control with Probabilistic Model Checking

TL;DR

This paper reviews advances in probabilistic model checking for multi-agent systems, emphasizing its applications in AI, robotics, and autonomous systems, and discusses challenges for future research.

Contribution

It summarizes recent developments in probabilistic model checking for multi-agent systems and explores its potential and challenges in various application domains.

Findings

Probabilistic model checking effectively verifies multi-agent interactions.

Integration of game theory enhances reasoning about rational agents.

Applications span AI, robotics, and autonomous systems.

Abstract

Probabilistic model checking is a technique for formal automated reasoning about software or hardware systems that operate in the context of uncertainty or stochasticity. It builds upon ideas and techniques from a diverse range of fields, from logic, automata and graph theory, to optimisation, numerical methods and control. In recent years, probabilistic model checking has also been extended to integrate ideas from game theory, notably using models such as stochastic games and solution concepts such as equilibria, to formally verify the interaction of multiple rational agents with distinct objectives. This provides a means to reason flexibly about agents acting in either an adversarial or a collaborative fashion, and opens up opportunities to tackle new problems within, for example, artificial intelligence, robotics and autonomous systems. In this paper, we summarise some of the advances in this area, and highlight applications for which they have already been used. We discuss how the strengths of probabilistic model checking apply, or have the potential to apply, to the multi-agent setting and outline some of the key challenges required to make further progress in this field.