Iterated Boolean games for rational verification

Conference item

Rational verification is the problem of understanding what temporal logic properties hold of a multi-agent system when agents are modelled as players in a game, each acting rationally in pursuit of personal preferences. More specifically, rational verification asks whether a given property, expressed as a temporal logic formula, is satisfied in a computation of the system that might be generated if agents within the system choose strategies for selecting actions that form a Nash equilibrium. We show that, when agents are modelled using the Simple Reactive Modules Language, a widely-used system modelling language for concurrent and multi-agent systems, this problem can be reduced to a simpler query: whether some iterated game—in which players have control over a finite set of Boolean variables and goals expressed as Linear Temporal Logic (LTL) formulae—has a Nash equilibrium. To better understand the complexity of solving this kind of verification problem in practice, we then study the two-player case for various types of LTL goals, present some experimental results, and describe a general technique to implement rational verification using MCMAS, a model checking tool for the verification of concurrent and multi-agent systems.

Authors: Gutierrez, J; Gao, T; Wooldridge, M

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Association for Computing Machinery
• Host title: 6th International Conference on Autonomous Agents and Multiagent Systems - AAMAS 2017
• Journal: 6th International Conference on Autonomous Agents and Multiagent Systems - AAMAS 2017
• Publication date: 2017-05-01
• Acceptance date: 2017-01-24
• Keywords: Formal Verification; Linear Temporal Logic; MCMAS; Nash Equilibria; Iterated Boolean Games; Strategy Logic