Verification of Cooperative and Concurrent Multi-Player Mean-Payoff Games
Talk, Invited talk at the Understandable Autonomous System Seminar, School of Computing Science, University of Glasgow,
Talks and presentations
Game Theory Meets AI: A Logical and Mathematical Approach to Verifying Multi-Agent Systems
Talk, Keynote talk at the International Conference on Applied Mathematics, Statistics, and Computing 2023, Udayana University, Bali, Indonesia
Examining Games and a Way to Repair Them
Talk, Invited talk at *WhiteMech Group Meetings, Department of Computer, Control, and Management Engineering, Sapienza University of Rome,
Classical notion of correctness in formal verification is not appropriate for multi-agent systems–it does not capture the strategic behaviour of rational agents. As such, a different concept of correctness was proposed in rational verification. In proving such a correctness, we turn multi-agent systems into multi-player games and use game-theoretic techniques to analyse the games. In our works, we study various kinds of games with various goals and settings, and provide an algorithmic techniques to solve problems related to rational verification. We also propose a method to “repair” games should we find them “broken”. Slides
Automated Temporal Equilibrium Analysis: Verification and Synthesis of Multi-Player Games
Talk, Journal track of the 30th International Joint Conference on Artificial Intelligence (IJCAI 2021),
Equilibrium Design for Concurrent Games
Talk, 8th International Workshop on Strategic Reasoning (Satellite Workshop of ECAI 2020),
In game theory, mechanism design is concerned with the design of incentives so that a desired outcome of the game can be achieved. In this paper, we study the design of incentives so that a desirable equilibrium is obtained, for instance, an equilibrium satisfying a given temporal logic property—a problem that we call equilibrium design. We base our study on a framework where system specifications are represented as temporal logic formulae, games as quantitative concurrent game structures, and players’ goals as mean-payoff objectives. In particular, we consider system specifications given by LTL and GR(1) formulae, and show that implementing a mechanism to ensure that a given temporal logic property is satisfied on some/every Nash equilibrium of the game, whenever such a mechanism exists, can be done in PSPACE for LTL properties and in NP/$\Sigma^P_2$ for GR(1) specifications. We also study the complexity of various related decision and optimisation problems, such as optimality and uniqueness of solutions, and show that the complexities of all such problems lie within the polynomial hierarchy. As an application, equilibrium design can be used as an alternative solution to the rational synthesis and verification problems for concurrent games with mean-payoff objectives whenever no solution exists, or as a technique to repair, whenever possible, concurrent games with undesirable rational outcomes (Nash equilibria) in an optimal way. Extended abstract Slides
Logic and Games
Talk, Guest lecture in Logic & Semantics of Programming Languages course (Winter Semester 2020), Department of Computer Science, TU Kaiserslautern.,
Verifying and Designing Equilibria in Multiagent Systems
Talk, 2nd International Workshop on Recent Advances in Concurrency and Logic (RADICAL 2019) (co-located with CONCUR 2019), Amsterdam, The Netherlands
Verifying equilibria involves checking which temporal logic properties will hold in some “stable” runs of a system composed of multiple agents which are assumed to behave rationally and strategically in pursuit of individual objectives. This paradigm is called rational verification, and can be regarded as a counterpart to (classical) model checking for multi-agent systems. In this talk, I will propose a practically amenable technique for rational verification which relies on a reduction to the solution of a collection of parity games. This approach has been implemented in a tool called EVE. I will also talk about some cases in which the problem of rational verification is computationally tractable. In particular, it is possible to reduce the complexity from 2EXPTIME to fixed-parameter tractable. Finally, I will also introduce a concept called equilibrium design which is concerned in the design of incentives so that a desirable equilibrium is obtained. Extended abstract Slides
Some Approaches to Rational Verification in Multiagent Systems
Talk, 1st International Workshop on Recent Advances in Concurrency and Logic (RADICAL 2017) (co-located with CONCUR 2017), Berlin, Germany
Recently, with the rapid advances of artificial intelligence, many researchers from verification community are starting to work on the analysis of systems composed of (semi)autonomous components known as multiagent systems. With this increasing interest, many concepts for reasoning about the behaviour of such systems are proposed. Among them is rational verification which is concerned with establishing whether a property can be sustained in a system composed of rational agents. In our research, we study different approaches to realise the notion of rational verification and strive for a concrete tool implementing the paradigm. We begin by introducing a formal framework as the foundation of our approaches. We then discuss the ability of current techniques/tools to perform rational verification and present some methods we have developed to expand the limits. We conclude with our ongoing work and possible future directions. Extended Abstract Slides