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