Supervisor

Suitable for

Abstract

EVE (Equilibrium Verification Environment) is a formal verification tool for the automated analysis of temporal equilibrium properties of concurrent and multi-agent systems represented as multi-player games. In EVE, systems are modelled using the Simple Reactive Module Language (SRML) as a collection of independent system components (players/agents in a game), which are assumed to have goals expressed using Linear Temporal Logic (LTL) formulae. EVE can be used to check the existence of Nash equilibria in such systems and verify which temporal logic properties are satisfied in the equilibria, problems that belong to the Rational Verification framework. The goal of this project is to extend the verification capabilities of EVE, either through the implementation of new or already existing algorithms for Rational Verification.

Prerequisites: Discrete Mathematics; Computer-Aided Formal Verification, Computational Complexity

Desirable: Automata, Logic and Games; Computational Game Theory Project type: Practice