EVE (Equilibrium Verification Environment)
EVE is a formal verification tool for the automated analysis of temporal equilibrium properties of concurrent and multi-agent systems represented as multi-player games
EVE is a formal verification tool for the automated analysis of temporal equilibrium properties of concurrent and multi-agent systems represented as multi-player games
This tool takes SRML file as an input and convert it to ISPL. It then runs MCMAS to check NE-Emptiness of the setting. Currently supporting memoryless fragment of SL.
Published in the 16th International Symposium on Automated Technology for Verification and Analysis (ATVA 2018), Los Angeles, USA, 2018
Download here
Published in the 28th International Joint Conference on Artificial Intelligence (IJCAI 2019), Macao, China, 2019
Download here
Published in The 30th International Conference on Concurrency Theory (CONCUR 2019), Amsterdam, the Netherlands, 2019
Download here
Published in Artificial Intelligence, 2020
Download here
Published in The 18th Asian Symposium on Programming Languages and Systems (APLAS), 2020
Download here
Published in Applied Intelligence, 2021
Download here
Published in The 18th International Conference on Principles of Knowledge Representation and Reasoning (KR 2021), 2021
Download here
Published in Annals of Mathematics and Artificial Intelligence, 2022
Download here
Published in 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024), Naples, Italy, 2024
Download here
Published in 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024), Naples, Italy, 2024
Download here
Published in Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence (IJCAI-24), 2024
Download here
Published in Proceedings of the 27th European Conference on Artificial Intelligence (ECAI-24), 2024
Download here
Published in Logical Methods in Computer Science, 2024
Download here
Published:
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
Published:
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
Published:
Published:
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
Published:
Published:
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
Published:
Lab Demonstrator, Department of Computer Science, University of Oxford, 2016
Lab sessions for Intelligent Systems course (Michaelmas Term 2016) in the Department of Computer Science, University of Oxford.
Lab Demonstrator, Department of Computer Science, University of Oxford, 2017
Lab sessions for Intelligent Systems course (Michaelmas Term 2017) in the Department of Computer Science, University of Oxford.
Tutor, Department of Computer Science, University of Oxford, 2018
Class tutor for Logic and Proof course (Hilary Term 2018) in the Department of Computer Science, University of Oxford.
Tutor, Department of Computer Science, University of Oxford, 2018
Class tutor for Computational Game Theory course (Michaelmas Term 2018) in the Department of Computer Science, University of Oxford.
Teaching Assistant, EPSRC Centre for Doctoral Training on Autonomous, Intelligent Machines, and Systems (AIMS), University of Oxford, 2019
Teaching assistant for Computational Game Theory course (Hilary Term 2019) at EPSRC Centre for Doctoral Training on Autonomous, Intelligent Machines, and Systems (AIMS), University of Oxford
Tutorial Organiser, Department of Computer Science, University of Kaiserslautern, 2019
Tutorials, exercises, and final exams organisation for Logic and Semantics of Programming Languages course winter semester 2019.
Co-Lecturer (with Prof. Anthony Lin and Dr Daniel Stan), Department of Computer Science, University of Kaiserslautern, 2021
Lecturer, School of Mathematical and Computer Sciences, Heriot-Watt University, 2022
Lecturer, School of Mathematical and Computer Sciences, Heriot-Watt University, 2024
Lecturer, School of Mathematical and Computer Sciences, Heriot-Watt University, 2024