Rational Verification

TBA

Michael Wooldridge (University of Oxford), Julian Gutierrez (Monash University) 

Contact email: Julian.Gutierrez@monash.edu 

• A level of understanding of logic that would typically be acquired in an undergraduate computer science course. 

• No knowledge of game theory. 

• Some understanding of complexity theory would be helpful (at the level of P vs. NP).

• Understanding theory and algorithms for rational verification

• Using EVE, a formal verification tool

In the context of multi-agent systems, the rational verification problem is concerned with checking which properties will hold in a system when its constituent agents are assumed to behave rationally and strategically in pursuit of individual objectives. In many ways, rational verification is a natural game-theoretic counterpart of the conventional model checking problem in the automated/formal verification of computing systems. In this tutorial, we will introduce the theory and associated algorithms and practical implementation of the rational verification framework for concurrent and multi-agent systems. Specifically, the participants will be introduced to the basics of logic and game theory behind rational verification, and will learn about concrete algorithmic techniques that can be used in practice to automatically analyse the behaviour of complex multi-agent systems. Assuming only a background that would be obtained from an undergraduate course in computing, we will introduce the main models, decision problems, and algorithms begind rational verification. The tutorial will also present EVE, a formal verification tool that implements the most important decision procedures behind the rational verification framework. We will not assume any detailed prior knowledge on temporal logic, formal verification, or game theory.