Author name cluster

David Hyland

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

8 papers

2 author rows

IJCAI Conference 2024 Conference Paper

Endogenous Energy Reactive Modules Games: Modelling Side Payments among Resource-Bounded Agents

Julian Gutierrez
David Hyland
Muhammad Najib
Giuseppe Perelli
Michael Wooldridge

We introduce Energy Reactive Modules Games (ERMGs), an extension of Reactive Modules Games (RMGs) in which actions incur an energy cost (which may be positive or negative), and the choices that players make are restricted by the energy available to them. In ERMGs, each action is associated with an energy level update, which determines how their energy level is affected by the performance of the action. In addition, agents are provided with an initial energy allowance. This allowance plays a crucial role in shaping an agent’s behaviour, as it must be taken into consideration when one is determining their strategy: agents may only perform actions if they have the requisite energy. We begin by studying rational verification for ERMGs and then introduce Endogenous ERMGs, where agents can choose to transfer their energy to other agents. This exchange may enable equilibria that are impossible to achieve without such transfers. We study the decision problem of whether a stable outcome exists under both the Nash equilibrium and Core solution concepts.

PDF Details DOI

KR Conference 2024 Conference Paper

Incentive Design for Rational Agents

David Hyland
Munyque Mittelmann
Aniello Murano
Giuseppe Perelli
Michael Wooldridge

We introduce Incentive Design: a new class of problems for equilibrium verification in multi-agent systems. In our model, agents attempt to maximize their utility functions, which are expressed as formulae in LTL[F], a quantitative extension of Linear Temporal Logic with functions computable in polynomial time. We assume agents are rational, in the sense that they adopt strategies consistent with game theoretic solution concepts such as Nash equilibrium. For each solution concept we consider, we analyze the problems of verifying whether an incentive scheme achieves a societal objective and finding one that does so, whether it be social welfare or any other aggregate measure of collective well-being. We study both static and dynamic incentive schemes, showing that the latter are more powerful than the former. Finally, we solve the incentive verification and synthesis problems for all the solution concepts we consider, and analyze their complexity.

PDF Details DOI

AAMAS Conference 2024 Conference Paper

Rational Verification with Quantitative Probabilistic Goals

David Hyland
Julian Gutierrez
Krishna Shankaranarayanan
Michael Wooldridge

We study the rational verification problem for multi-agent systems in a setting where agents have quantitative probabilistic goals. We use concurrent stochastic games to model multi-agent systems and assume players desire to maximise the probability of satisfying their goals, specified using Linear Temporal Logic (LTL). The main decision problem in this setting is whether a given LTL formula is almost surely satisfied on some pure Nash equilibrium of a given game. We prove that this problem is undecidable in the general case, and then characterise the complexity of this problem under various restrictions on strategies. We also study the problem of deciding whether a given strategy profile is a Nash equilibrium in a given game and show that, unlike the previous verification problem, this question is decidable for several common strategy models.

PDF

TARK Conference 2023 Conference Paper

Incentive Engineering for Concurrent Games

David Hyland
Julian Gutierrez 0001
Michael J. Wooldridge

We consider the problem of incentivising desirable behaviours in multi-agent systems by way of taxation schemes. Our study employs the concurrent games model: in this model, each agent is primarily motivated to seek the satisfaction of a goal, expressed as a Linear Temporal Logic (LTL) formula; secondarily, agents seek to minimise costs, where costs are imposed based on the actions taken by agents in different states of the game. In this setting, we consider an external principal who can influence agents' preferences by imposing taxes (additional costs) on the actions chosen by agents in different states. The principal imposes taxation schemes to motivate agents to choose a course of action that will lead to the satisfaction of their goal, also expressed as an LTL formula. However, taxation schemes are limited in their ability to influence agents' preferences: an agent will always prefer to satisfy its goal rather than otherwise, no matter what the costs. The fundamental question that we study is whether the principal can impose a taxation scheme such that, in the resulting game, the principal's goal is satisfied in at least one or all runs of the game that could arise by agents choosing to follow game-theoretic equilibrium strategies. We consider two different types of taxation schemes: in a static scheme, the same tax is imposed on a state-action profile pair in all circumstances, while in a dynamic scheme, the principal can choose to vary taxes depending on the circumstances. We investigate the main game-theoretic properties of this model as well as the computational complexity of the relevant decision problems.

Details DOI

LAMAS&SR Workshop 2023 Workshop Paper

Incentive Engineering for Concurrent Games

David Hyland

We consider the problem of incentivising desirable behaviours in multi-agent systems by way of taxation schemes. Our study employs the concurrent games model: in this model, each agent is primarily motivated to seek the satisfaction of a goal, expressed as a Linear Temporal Logic (LTL) formula; secondarily, agents seek to minimise costs, where costs are imposed based on the actions taken by agents in different states of the game. In this setting, we consider an external principal who can influence agents’ preferences by imposing taxes (additional costs) on the actions chosen by agents in different states. The principal imposes taxation schemes to motivate agents to choose a course of action that will lead to the satisfaction of their goal, also expressed as an LTL formula. However, taxation schemes are limited in their ability to influence agents’ preferences: an agent will always prefer to satisfy its goal rather than otherwise, no matter what the costs. The fundamental question that we study is whether the principal can impose a taxation scheme such that, in the resulting game, the principal’s goal is satisfied in at least one or all runs of the game that could arise by agents choosing to follow game-theoretic equilibrium strategies. We consider two different types of taxation schemes: in a static scheme, the same tax is imposed on a state-action profile pair in all circumstances, while in a dynamic scheme, the principal can choose to vary taxes depending on the circumstances. We investigate the main game-theoretic properties of this model as well as the computational complexity of the relevant decision problems.

Details

AAMAS Conference 2023 Conference Paper

k -Prize Weighted Voting Game

Wei-Chen Lee
David Hyland
Alessandro Abate
Edith Elkind
Jiarui Gan
Julian Gutierrez
Paul Harrenstein
Michael Wooldridge

We introduce a natural variant of weighted voting games, which we refer to as 𝑘-Prize Weighted Voting Games. Such games consist of 𝑛 players with weights, and 𝑘 prizes, of possibly differing values. The players form coalitions, and the 𝑖-th largest coalition (by the sum of weights of its members) wins the 𝑖-th largest prize, which is then shared among its members. We present four solution concepts to analyse the games in this class, and characterise the existence of stable outcomes in games with three players and two prizes, and in games with uniform prizes. We then explore the efficiency of stable outcomes in terms of Pareto optimality and utilitarian social welfare. Finally, we study the computational complexity of finding stable outcomes.

PDF

ECAI Conference 2023 Conference Paper

Learning Task Automata for Reinforcement Learning Using Hidden Markov Models

Alessandro Abate
Yousif Almulla
James Fox
David Hyland
Michael J. Wooldridge

Training reinforcement learning (RL) agents using scalar reward signals is often infeasible when an environment has sparse and non-Markovian rewards. Moreover, handcrafting these reward functions before training is prone to misspecification. We learn non-Markovian finite task specifications as finite-state ‘task automata’ from episodes of agent experience within environments with unknown dynamics. First, we learn a product MDP, a model composed of the specification’s automaton and the environment’s MDP (both initially unknown), by treating it as a partially observable MDP and employing a hidden Markov model learning algorithm. Second, we efficiently distil the task automaton (assumed to be a deterministic finite automaton) from the learnt product MDP. Our automaton enables a task to be decomposed into sub-tasks, so an RL agent can later synthesise an optimal policy more efficiently. It is also an interpretable encoding of high-level task features, so a human can verify that the agent’s learnt tasks have no misspecifications. Finally, we also take steps towards ensuring that the automaton is environment-agnostic, making it well-suited for use in transfer learning.

Details

IJCAI Conference 2023 Conference Paper

Principal-Agent Boolean Games

David Hyland
Julian Gutierrez
Michael Wooldridge

We introduce and study a computational version of the principal-agent problem -- a classic problem in Economics that arises when a principal desires to contract an agent to carry out some task, but has incomplete information about the agent or their subsequent actions. The key challenge in this setting is for the principal to design a contract for the agent such that the agent's preferences are then aligned with those of the principal. We study this problem using a variation of Boolean games, where multiple players each choose valuations for Boolean variables under their control, seeking the satisfaction of a personal goal formula. In our setting, the principal can only observe some subset of these variables, and the principal chooses a contract which rewards players on the basis of the assignments they make for the variables that are observable to the principal. The principal's challenge is to design a contract so that, firstly, the principal's goal is achieved in some or all Nash equilibrium choices, and secondly, that the principal is able to verify that their goal is satisfied. In this paper, we formally define this problem and completely characterise the computational complexity of the most relevant decision problems associated with it.

PDF Details DOI