Julian Gutierrez

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.

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.

AIJ Journal 2023 Journal Article

Cooperative concurrent games

• Julian Gutierrez
• Szymon Kowara
• Sarit Kraus
• Thomas Steeples
• Michael Wooldridge

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.

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.

Highlights Conference 2021 Conference Abstract

Cooperative Concurrent Games

• Julian Gutierrez

Rational verification is the problem of determining which temporal logic properties will hold in a multi-agent system, under the assumption that agents in the system act rationally, by choosing strategies that collectively form a game theoretic equilibrium. Previous work in this area has largely focussed on non-cooperative games, with Nash equilibrium and a number of variants as the main game-theoretic solution concepts. Here, we extend the rational verification framework to cooperative games, in which players may form coalitions to collectively achieve their goals, and base our study on the core as our basic solution concept. In particular, we have developed the theory and algorithms for rational verification in both deterministic and probabilistic systems, using concurrent game structures (CGS) and concurrent stochastic games (CSG), respectively, as models. We show that if players’ goals are given by LTL formulae, regardless of the type of solution concept (Nash equilibrium or the core) or underlying model (CGS or CSG), solving such multi-player games can be done in 2EXPTIME, but in each case requiring rather different proof techniques.

LAMAS&SR Workshop 2021 Workshop Paper

Mean-Payoff Games with Omega-Regular Specifications

• Thomas Steeples
• Julian Gutierrez
• Michael Wooldridge

Multi-player mean-payoff games are a natural formalism for modelling the behaviour of concurrent and multi-agent systems with self-interested players. Players in such a game traverse a graph, while trying to maximise a mean-payoff function that depends on the plays so generated. As with all games, the equilibria that could arise may have undesirable properties. However, as system designers, we typically wish to ensure that equilibria in such systems correspond to desirable system behaviours, for example, satisfying certain safety or liveness properties. One natural way to do this would be to specify such desirable properties using temporal logic. Unfortunately, the use of temporal logic specifications causes game theoretic verification problems to have very high computational complexity. To this end, we consider 𝜔-regular specifications, which offer a concise and intuitive way of specifying desirable behaviours of a system. The main results of this work are characterisation and complexity bounds for the problem of determining if there are equilibria that satisfy a given 𝜔-regular specification in a multiplayer mean-payoff game in a number of computationally relevant game-theoretic settings.

AAMAS Conference 2021 Conference Paper

Mean-Payoff Games with ω-Regular Specifications

• Thomas Steeples
• Julian Gutierrez
• Michael Wooldridge

Multi-player mean-payoff games are a natural formalism to model concurrent and multi-agent systems with self-interested players. Players in such a game traverse a graph, while trying to maximise a mean-payoff function that depends on the plays so generated. As with all games, the equilibria that could arise may have undesirable properties. However, as system designers, we typically wish to ensure that equilibria in such systems correspond to desirable system behaviours, for example, satisfying certain safety or liveness properties. One natural way to do this would be to specify such desirable properties using temporal logic. Unfortunately, the use of temporal logic specifications causes game theoretic verification problems to have very high computational complexity. To this end, we consider ω-regular specifications, which offer a concise and intuitive way of specifying desirable behaviours of a system. The main results of this work are characterisation and complexity bounds for the problem of determining if there are equilibria that satisfy a given ω-regular specification in a multi-player mean-payoff game in a number of computationally relevant game-theoretic settings.

AAMAS Conference 2021 Conference Paper

Multi-Agent Reinforcement Learning with Temporal Logic Specifications

• Lewis Hammond
• Alessandro Abate
• Julian Gutierrez
• Michael Wooldridge

In this paper, we study the problem of learning to satisfy temporal logic specifications with a group of agents in an unknown environment, which may exhibit probabilistic behaviour. From a learning perspective these specifications provide a rich formal language with which to capture tasks or objectives, while from a logic and automated verification perspective the introduction of learning capabilities allows for practical applications in large, stochastic, unknown environments. The existing work in this area is, however, limited. Of the frameworks that consider full linear temporal logic or have correctness guarantees, all methods thus far consider only the case of a single temporal logic specification and a single agent. In order to overcome this limitation, we develop the first multi-agent reinforcement learning technique for temporal logic specifications, which is also novel in its ability to handle multiple specifications. We provide correctness and convergence guarantees for our main algorithm – Almanac (Automaton/Logic Multi-Agent Natural Actor-Critic) – even when using function approximation. Alongside our theoretical results, we further demonstrate the applicability of our technique via a set of preliminary experiments.

KR Conference 2021 Conference Paper

Rational Verification for Probabilistic Systems

• Julian Gutierrez
• Lewis Hammond
• Anthony W. Lin
• Muhammad Najib
• Michael Wooldridge

Rational verification is the problem of determining which temporal logic properties will hold in a multi-agent system, under the assumption that agents in the system act rationally, by choosing strategies that collectively form a game-theoretic equilibrium. Previous work in this area has largely focussed on deterministic systems. In this paper, we develop the theory and algorithms for rational verification in probabilistic systems. We focus on concurrent stochastic games (CSGs), which can be used to model uncertainty and randomness in complex multi-agent environments. We study the rational verification problem for both non-cooperative games and cooperative games in the qualitative probabilistic setting. In the former case, we consider LTL properties satisfied by the Nash equilibria of the game and in the latter case LTL properties satisfied by the core. In both cases, we show that the problem is 2EXPTIME-complete, thus not harder than the much simpler verification problem of model checking LTL properties of systems modelled as Markov decision processes (MDPs).

AIJ Journal 2020 Journal Article

Automated temporal equilibrium analysis: Verification and synthesis of multi-player games

• Julian Gutierrez
• Muhammad Najib
• Giuseppe Perelli
• Michael Wooldridge

AAMAS Conference 2019 Conference Paper

Cooperative Concurrent Games

• Julian Gutierrez
• Sarit Kraus
• Michael Wooldridge

In rational verification, one is interested in understanding which temporal logic properties will hold in a concurrent game, under the assumption that players choose strategies that form an equilibrium. Players are assumed to behave rationally in pursuit of individual goals, typically specified as temporal logic formulae. To date, rational verification has only been studied in noncooperative settings. In this paper, we extend the rational verification framework to cooperative games, in which players may form coalitions to collectively achieve their goals. We base our study on the computational model given by concurrent game structures and focus on the core as our basic solution concept. We show the core of a concurrent game can be logically characterised using ATL*, and study the computational complexity of key decision problems associated with the core, which range from problems in PSPACE to problems in 3EXPTIME. We also discuss a number of variants of the main definition of the core, leading to the issue of credible coalition formations, and a possible implementation of the main reasoning framework.

IJCAI Conference 2019 Conference Paper

On Computational Tractability for Rational Verification

• Julian Gutierrez
• Muhammad Najib
• Giuseppe Perelli
• Michael Wooldridge

Rational verification involves checking which temporal logic properties hold of a concurrent and multiagent system, under the assumption that agents in the system choose strategies in game theoretic equilibrium. Rational verification can be understood as a counterpart of model checking for multiagent systems, but while model checking can be done in polynomial time for some temporal logic specification languages such as CTL, and polynomial space with LTL specifications, rational verification is much more intractable: it is 2EXPTIME-complete with LTL specifications, even when using explicit-state system representations. In this paper we show that the complexity of rational verification can be greatly reduced by restricting specifications to GR(1), a fragment of LTL that can represent most response properties of reactive systems. We also provide improved complexity results for rational verification when considering players' goals given by mean-payoff utility functions -- arguably the most widely used quantitative objective for agents in concurrent and multiagent systems. In particular, we show that for a number of relevant settings, rational verification can be done in polynomial space or even in polynomial time.

AAMAS Conference 2018 Conference Paper

Local Equilibria in Logic-Based Multi-Player Games

• Julian Gutierrez
• Paul Harrenstein
• Thomas Steeples
• Michael Wooldridge

Game theory provides a well-established framework for the analysis and verification of concurrent and multi-agent systems. Typically, the analysis of a multi-agent system involves computing the set of equilibria in the associated multi-player game representing the behaviour of the system. As systems grow larger, it becomes increasingly harder to find equilibria in the game – which represent the rationally stable behaviours of the multi-agent system (the solutions of the game). To address this issue, in this paper, we study the concept of local equilibria, which are defined with respect to (maximal) stable coalitions of agents for which an equilibrium can de found. We focus on the solutions given by the Nash equilibria of Boolean games and iterated Boolean games, two logic-based models for multi-agent systems, in which the players’ goals are given by formulae of propositional logic and LTL, respectively.

AIJ Journal 2017 Journal Article

From model checking to equilibrium checking: Reactive modules for rational verification

• Julian Gutierrez
• Paul Harrenstein
• Michael Wooldridge

AAMAS Conference 2017 Conference Paper

Iterated Boolean Games for Rational Verification

• Tong Gao
• Julian Gutierrez
• Michael Wooldridge

Rational verification is the problem of understanding what temporal logic properties hold of a multi-agent system when agents are modelled as players in a game, each acting rationally in pursuit of personal preferences. More specifically, rational verification asks whether a given property, expressed as a temporal logic formula, is satisfied in a computation of the system that might be generated if agents within the system choose strategies for selecting actions that form a Nash equilibrium. We show that, when agents are modelled using the Simple Reactive Modules Language, a widely-used system modelling language for concurrent and multi-agent systems, this problem can be reduced to a simpler query: whether some iterated game—in which players have control over a finite set of Boolean variables and goals expressed as Linear Temporal Logic (LTL) formulae—has a Nash equilibrium. To better understand the complexity of solving this kind of verification problem in practice, we then study the two-player case for various types of LTL goals, present some experimental results, and describe a general technique to implement rational verification using MCMAS, a model checking tool for the verification of concurrent and multi-agent systems.

AAMAS Conference 2017 Conference Paper

Iterated Games with LDL Goals over Finite Traces

• Julian Gutierrez
• Giuseppe Perelli
• Michael Wooldridge

Linear Dynamic Logic on finite traces (LDLF) is a powerful logic for reasoning about the behaviour of concurrent and multi-agent systems. In this paper, we investigate techniques for both the characterisation and verification of equilibria in multi-player games with goals/objectives expressed using logics based on LDLF. This study builds upon a generalisation of Boolean games, a logic-based game model of multi-agent systems where players have goals succinctly represented in a logical way. Because LDLF goals are considered, in the setting we study—iterated Boolean games with goals over finite traces (iBGF )—players’ goals can be defined to be regular properties while achieved in a finite, but arbitrarily large, trace. In particular, using alternating automata, the paper investigates automata-theoretic approaches to the characterisation and verification of (pure strategy Nash) equilibria, shows that the set of Nash equilibria in games with LDLF objectives is regular, and provides complexity results for the associated automata constructions. CCS Concepts •Computing methodologies → Multi-agent systems;

IJCAI Conference 2017 Conference Paper

Nash Equilibria in Concurrent Games with Lexicographic Preferences

• Julian Gutierrez
• Aniello Murano
• Giuseppe Perelli
• Sasha Rubin
• Michael Wooldridge

We study concurrent games with finite-memory strategies where players are given a Buchi and a mean-payoff objective, which are related by a lexicographic order: a player first prefers to satisfy its Buchi objective, and then prefers to minimise costs, which are given by a mean-payoff function. In particular, we show that deciding the existence of a strict Nash equilibrium in such games is decidable, even if players' deviations are implemented as infinite memory strategies.

AAMAS Conference 2016 Conference Paper

Expressiveness and Nash Equilibrium in Iterated Boolean Games

• Julian Gutierrez
• Paul Harrenstein
• Giuseppe Perelli
• Michael Wooldridge

We introduce and investigate a novel notion of expressiveness for temporal logics that is based on game theoretic properties of multiagent systems. We focus on iterated Boolean games, where each agent i has a goal γi, represented using (a fragment of) Linear Temporal Logic (LTL). The goal γi captures agent i’s preferences: the models of γi represent system behaviours that would satisfy i, and each player is assumed to act strategically, taking into account the goals of other players, in order to bring about computations satisfying their goal. In this setting, we apply the standard gametheoretic concept of Nash equilibria: the Nash equilibria of an iterated Boolean game can be understood as a (possibly empty) set of computations, each computation representing one way the system could evolve if players chose strategies in Nash equilibrium. Such an equilibrium set of computations can be understood as expressing a temporal property—which may or may not be expressible within a particular LTL fragment. The new notion of expressiveness that we study is then as follows: what LTL properties are characterised by the Nash equilibria of games in which agent goals are expressed in fragments of LTL? We formally define and investigate this notion of expressiveness and some related issues, for a range of LTL fragments.

KR Conference 2016 Conference Paper

ImperfectInformation in Reactive Modules Games

• Julian Gutierrez
• Giuseppe Perelli
• Michael Wooldridge

Reactive Modules is a high-level modelling language for concurrent, distributed, and multi-agent systems, which is used in a number of practical model checking tools. Reactive Modules Games are a game-theoretic extension of Reactive Modules, in which agents in a system are assumed to act strategically in an attempt to satisfy a temporal logic formula representing their individual goal. Reactive Modules Games with perfect information have been closely studied, and the complexity of game theoretic decision problems relating to such games have been comprehensively classified. However, to date, no work has considered the imperfect information case. In this paper we address this gap, investigating Reactive Modules Games in which agents have only partial visibility of their environment.

AAAI Conference 2016 Conference Paper

Rational Verification: From Model Checking to Equilibrium Checking

• Michael Wooldridge
• Julian Gutierrez
• Paul Harrenstein
• Enrico Marchioni
• Giuseppe Perelli
• Alexis Toumi

Rational verification is concerned with establishing whether a given temporal logic formula ϕ is satisfied in some or all equilibrium computations of a multi-agent system – that is, whether the system will exhibit the behaviour ϕ under the assumption that agents within the system act rationally in pursuit of their preferences. After motivating and introducing the framework of rational verification, we present formal models through which rational verification can be studied, and survey the complexity of key decision problems. We give an overview of a prototype software tool for rational verification, and conclude with a discussion and related work.

KR Conference 2014 Conference Paper

Reasoning about Equilibria in Game-like Concurrent Systems

• Julian Gutierrez
• Paul Harrenstein
• Michael Wooldridge

the assumption that they act rationally and strategically in pursuit of their goals. In this paper, we present a branching time logic that is explicitly intended for this purpose. Specifically, we provide a logic for reasoning about the equilibrium properties of game-like concurrent systems. Equilibrium concepts are the best-known and most widely applied analytical tools in the game theory literature, and of these Nash equilibrium is the best-known (Osborne and Rubinstein 1994). A Nash equilibrium is an outcome that obtains because no player has a rational incentive to deviate from it. If we consider Nash equilibrium in the context of game-like concurrent systems, then it is natural to ask which computations (runs, histories,...) will be generated in equilibrium? In (Gutierrez, Harrenstein, and Wooldridge 2013), this question was investigated using the Iterated Boolean Games (iBG) model. In this model, each player is assumed to control a set of Boolean variables, and the game is played over an infinite sequence of rounds, where at each round every player chooses values for its variables. Each player has a goal, expressed as an LTL formula, and acts strategically in pursuit of this goal. Given this, some computations of a game can be identified as being the result of Nash equilibrium strategies, and (Gutierrez, Harrenstein, and Wooldridge 2013) suggested that the key questions in the strategic analysis of the system are whether a given LTL formula holds in some or all equilibrium computations. While the iBG model of (Gutierrez, Harrenstein, and Wooldridge 2013) is useful for the purposes of exposition, it is not a realistic model of concurrent programs. Moreover, (Gutierrez, Harrenstein, and Wooldridge 2013) provides no language for reasoning about the equilibria of systems: such reasoning must be carried out at the meta-level. This paper fills those gaps. First, we present a computational model that is more appropriate for modelling concurrent systems than the iBG model. In this model, the goals (and thus preferences) of players are given as temporal logic formulae that the respective player aspires to satisfy. After exploring some properties of this model, we introduce Equilibrium Logic (EL) as a formalism for reasoning about the equilibria of such systems. EL is a branching time logic that provides a new path quantifier [NE]ϕ, which asserts that ϕ holds on all Nash equilibrium computations of the system. Thus, EL supports reasoning about equilibria directly in the object language. We then investigate some properties of this logic. Our aim is to develop techniques for reasoning about gamelike concurrent systems, where the components of the system act rationally and strategically in pursuit of logicallyspecified goals. We first present a computational model for such systems, and investigate its properties. We then define and investigate a branching-time logic for reasoning about the equilibrium properties of such systems. The key operator in this logic is a path quantifier [NE]ϕ, which asserts that ϕ holds on all Nash equilibrium computations of the system.

TCS Journal 2014 Journal Article

The μ-calculus alternation hierarchy collapses over structures with restricted connectivity

• Julian Gutierrez
• Felix Klaedtke
• Martin Lange

IJCAI Conference 2013 Conference Paper

Iterated Boolean Games

• Julian Gutierrez
• Paul Harrenstein
• Michael Wooldridge

Iterated games are well-known in the game theory literature. We study iterated Boolean games. These are games in which players repeatedly choose truth values for Boolean variables they have control over. Our model of iterated Boolean games assumes that players have goals given by formulae of Linear Temporal Logic (LTL), a formalism for expressing properties of state sequences. In order to model the strategies that players use in such games, we use a finite state machine model. After introducing and formally defining iterated Boolean games, we investigate the computational complexity of their associated game-theoretic decision problems as well as semantic conditions characterising classes of LTL properties that are preserved by pure strategy Nash equilibria whenever they exist.

GandALF Workshop 2012 Workshop Paper

The μ-Calculus Alternation Hierarchy Collapses over Structures with Restricted Connectivity

• Julian Gutierrez
• Felix Klaedtke
• Martin Lange

It is known that the alternation hierarchy of least and greatest fixpoint operators in the mu-calculus is strict. However, the strictness of the alternation hierarchy does not necessarily carry over when considering restricted classes of structures. A prominent instance is the class of infinite words over which the alternation-free fragment is already as expressive as the full mu-calculus. Our current understanding of when and why the mu-calculus alternation hierarchy is not strict is limited. This paper makes progress in answering these questions by showing that the alternation hierarchy of the mu-calculus collapses to the alternation-free fragment over some classes of structures, including infinite nested words and finite graphs with feedback vertex sets of a bounded size. Common to these classes is that the connectivity between the components in a structure from such a class is restricted in the sense that the removal of certain vertices from the structure's graph decomposes it into graphs in which all paths are of finite length. Our collapse results are obtained in an automata-theoretic setting. They subsume, generalize, and strengthen several prior results on the expressivity of the mu-calculus over restricted classes of structures.