View Proposal


Proposer
Muhammad Najib
Title
Rational Verification for Mean-Payoff Games
Goal
Description
Rational verification is the problem of checking whether a given temporal logic formula Ï• is satisfied in some or all game-theoretic equilibria of a multi-agent system. EVE (Equilibrium Verification Environment) is a tool for rational verification. Currently, EVE only support games with LTL objectives. In this project, you will extend EVE to support games with mean-payoff objectives. In particular, you will do the following - Extend EVE (https://github.com/eve-mas/eve-parity) to multi-player mean-payoff games - Implement algorithm in [1] to solve relevant decision problems - Integrate mean-payoff solver to EVE, e.g., https://github.com/romainbrenguier/MeanPayoffSolver Reference: [1] Gutierrez, Julian, et al. "On computational tractability for rational verification." International Joint Conferences on Artificial Intelligence, 2019.
Resources
Background
Automata theory, Python
Url
Difficulty Level
Challenging
Ethical Approval
None
Number Of Students
1
Supervisor
Muhammad Najib
Keywords
formal verification, model checking, multiagent systems, game theory
Degrees
Bachelor of Science in Computer Science
Master of Engineering in Software Engineering
Master of Science in Artificial Intelligence
Master of Science in Artificial Intelligence with SMI
Master of Science in Robotics
Master of Science in Software Engineering