Julian Gutierrez

"Games, Logic, and Formal Verification"

Multiplayer games provide a formal framework for the analysis of systems consisting of multiple agents, potentially exhibiting autonomous and intelligent behaviour. In this framework, the behaviour of such agents is restricted by an underlying graph-based structure that determines the states and actions of the agents in the system. Following the game-theoretic approach, agents in a system are seen as players in a game, with players' goals given in some formal specification language and optimal behaviour determined by a game-theoretic solution concept. In this talk, I will present a technique for the analysis of multi-player games -- and therefore of multi-agent systems -- where players' goals are given in logical form using Linear Temporal Logic (LTL), an extension of propositional logic with temporal logic modalities, and optimal behaviour given by the set of Nash equilibria in the game. We have shown that these multiplayer games, which can naturally be used for the automated synthesis and verification of multi-agent AI systems, can be solved in doubly exponential time, even when the description of the game/system is given using a high-level system description language. Our solution, for which we provide optimal complexity upper and lower bounds for 2EXPTIME, goes through a reduction to the solution of a collection of simpler parity games on graphs and Streett automata on infinite words. The main decision procedures have also been implemented in practice using EVE (Equilibrium Verification Environment), a software verification tool for the automated temporal equilibrium analysis of concurrent and multi-agent systems. EVE is free and available online at: http://eve.cs.ox.ac.uk/ Most of the results I will present were obtained through joint work with Muhammad Najib, Giuseppe Perelli, and Michael Wooldridge.

Termin als Datei downloaden und in den Kalender importieren.