Muhammad Najib

Muhammad Najib

Assistant Professor

Sitemap

A list of all the posts and pages found on the site. For you robots out there is an XML version available for digesting as well.

Pages

Posts

Future Blog Post

less than 1 minute read

Published:

This post will show up by default. To disable scheduling of future posts, edit config.yml and set future: false.

Blog Post number 4

less than 1 minute read

Published:

This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.

Blog Post number 3

less than 1 minute read

Published:

This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.

Blog Post number 2

less than 1 minute read

Published:

This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.

Blog Post number 1

less than 1 minute read

Published:

This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.

portfolio

publications

talks

Some Approaches to Rational Verification in Multiagent Systems

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

Verifying and Designing Equilibria in Multiagent Systems

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

Equilibrium Design for Concurrent Games

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

Examining Games and a Way to Repair Them

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

teaching

Intelligent Systems

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.

Intelligent Systems

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.

Logic and Proof

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.

Computational Game Theory

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.

Computational Game Theory

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

Logic and Semantics of Programming Languages

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.