Search Results

Documents authored by Gutierrez, Julian

Document
DOI: 10.4230/LIPIcs.CSL.2024.32
Characterising and Verifying the Core in Concurrent Multi-Player Mean-Payoff Games

Authors: Julian Gutierrez, Anthony W. Lin, Muhammad Najib, Thomas Steeples, and Michael Wooldridge

Published in: LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)

Abstract
Concurrent multi-player mean-payoff games are important models for systems of agents with individual, non-dichotomous preferences. Whilst these games have been extensively studied in terms of their equilibria in non-cooperative settings, this paper explores an alternative solution concept: the core from cooperative game theory. This concept is particularly relevant for cooperative AI systems, as it enables the modelling of cooperation among agents, even when their goals are not fully aligned. Our contribution is twofold. First, we provide a characterisation of the core using discrete geometry techniques and establish a necessary and sufficient condition for its non-emptiness. We then use the characterisation to prove the existence of polynomial witnesses in the core. Second, we use the existence of such witnesses to solve key decision problems in rational verification and provide tight complexity bounds for the problem of checking whether some/every equilibrium in a game satisfies a given LTL or GR(1) specification. Our approach is general and can be adapted to handle other specifications expressed in various fragments of LTL without incurring additional computational costs.
Cite as

Julian Gutierrez, Anthony W. Lin, Muhammad Najib, Thomas Steeples, and Michael Wooldridge. Characterising and Verifying the Core in Concurrent Multi-Player Mean-Payoff Games. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 32:1-32:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{gutierrez_et_al:LIPIcs.CSL.2024.32,
  author =	{Gutierrez, Julian and Lin, Anthony W. and Najib, Muhammad and Steeples, Thomas and Wooldridge, Michael},
  title =	{{Characterising and Verifying the Core in Concurrent Multi-Player Mean-Payoff Games}},
  booktitle =	{32nd EACSL Annual Conference on Computer Science Logic (CSL 2024)},
  pages =	{32:1--32:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-310-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{288},
  editor =	{Murano, Aniello and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.32},
  URN =		{urn:nbn:de:0030-drops-196752},
  doi =		{10.4230/LIPIcs.CSL.2024.32},
  annote =	{Keywords: Concurrent games, multi-agent systems, temporal logic, game theory}
}
Document
DOI: 10.4230/LIPIcs.TIME.2022.15
Giving Instructions in Linear Temporal Logic

Authors: Julian Gutierrez, Sarit Kraus, Giuseppe Perelli, and Michael Wooldridge

Published in: LIPIcs, Volume 247, 29th International Symposium on Temporal Representation and Reasoning (TIME 2022)

Abstract
Our aim is to develop a formal semantics for giving instructions to taskable agents, to investigate the complexity of decision problems relating to these semantics, and to explore the issues that these semantics raise. In the setting we consider, agents are given instructions in the form of Linear Temporal Logic (LTL) formulae; the intuitive interpretation of such an instruction is that the agent should act in such a way as to ensure the formula is satisfied. At the same time, agents are assumed to have inviolable and immutable background safety requirements, also specified as LTL formulae. Finally, the actions performed by an agent are assumed to have costs, and agents must act within a limited budget. For this setting, we present a range of interpretations of an instruction to achieve an LTL task Υ, intuitively ranging from "try to do this but only if you can do so with everything else remaining unchanged" up to "drop everything and get this done." For each case we present a formal pre-/post-condition semantics, and investigate the computational issues that they raise.
Cite as

Julian Gutierrez, Sarit Kraus, Giuseppe Perelli, and Michael Wooldridge. Giving Instructions in Linear Temporal Logic. In 29th International Symposium on Temporal Representation and Reasoning (TIME 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 247, pp. 15:1-15:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{gutierrez_et_al:LIPIcs.TIME.2022.15,
  author =	{Gutierrez, Julian and Kraus, Sarit and Perelli, Giuseppe and Wooldridge, Michael},
  title =	{{Giving Instructions in Linear Temporal Logic}},
  booktitle =	{29th International Symposium on Temporal Representation and Reasoning (TIME 2022)},
  pages =	{15:1--15:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-262-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{247},
  editor =	{Artikis, Alexander and Posenato, Roberto and Tonetta, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2022.15},
  URN =		{urn:nbn:de:0030-drops-172622},
  doi =		{10.4230/LIPIcs.TIME.2022.15},
  annote =	{Keywords: Linear Temporal Logic, Synthesis, Game theory, Multi-Agent Systems}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.22
Equilibrium Design for Concurrent Games

Authors: Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, and Michael Wooldridge

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract
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.
Cite as

Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, and Michael Wooldridge. Equilibrium Design for Concurrent Games. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 22:1-22:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{gutierrez_et_al:LIPIcs.CONCUR.2019.22,
  author =	{Gutierrez, Julian and Najib, Muhammad and Perelli, Giuseppe and Wooldridge, Michael},
  title =	{{Equilibrium Design for Concurrent Games}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{22:1--22:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.22},
  URN =		{urn:nbn:de:0030-drops-109246},
  doi =		{10.4230/LIPIcs.CONCUR.2019.22},
  annote =	{Keywords: Games, Temporal logic, Synthesis, Model checking, Nash equilibrium}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.17
Nash Equilibrium and Bisimulation Invariance

Authors: Julian Gutierrez, Paul Harrenstein, Giuseppe Perelli, and Michael Wooldridge

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
Game theory provides a well-established framework for the analysis of concurrent and multi-agent systems. The basic idea is that concurrent processes (agents) can be understood as corresponding to players in a game; plays represent the possible computation runs of the system; and strategies define the behaviour of agents. Typically, strategies are modelled as functions from sequences of system states to player actions. Analysing a system in such a way involves computing the set of (Nash) equilibria in the game. However, we show that, with respect to the above model of strategies---the standard model in the literature---bisimilarity does not preserve the existence of Nash equilibria. Thus, two concurrent games which are behaviourally equivalent from a semantic perspective, and which from a logical perspective satisfy the same temporal formulae, nevertheless have fundamentally different properties from a game theoretic perspective. In this paper we explore the issues raised by this discovery, and investigate three models of strategies with respect to which the existence of Nash equilibria is preserved under bisimilarity. We also use some of these models of strategies to provide new semantic foundations for logics for strategic reasoning, and investigate restricted scenarios where bisimilarity can be shown to preserve the existence of Nash equilibria with respect to the conventional model of strategies in the literature.
Cite as

Julian Gutierrez, Paul Harrenstein, Giuseppe Perelli, and Michael Wooldridge. Nash Equilibrium and Bisimulation Invariance. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 17:1-17:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{gutierrez_et_al:LIPIcs.CONCUR.2017.17,
  author =	{Gutierrez, Julian and Harrenstein, Paul and Perelli, Giuseppe and Wooldridge, Michael},
  title =	{{Nash Equilibrium and Bisimulation Invariance}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{17:1--17:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.17},
  URN =		{urn:nbn:de:0030-drops-77902},
  doi =		{10.4230/LIPIcs.CONCUR.2017.17},
  annote =	{Keywords: Bisumulation, Nash equilibrium, Multiagent systems, Strategy logic}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.268
Expresiveness and Complexity Results for Strategic Reasoning

Authors: Julian Gutierrez, Paul Harrenstein, and Michael Wooldridge

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
This paper presents a range of expressiveness and complexity results for the specification, computation, and verification of Nash equilibria in multi-player non-zero-sum concurrent games in which players have goals expressed as temporal logic formulae. Our results are based on a novel approach to the characterisation of equilibria in such games: a semantic characterisation based on winning strategies and memoryful reasoning. This characterisation allows us to obtain a number of other results relating to the analysis of equilibrium properties in temporal logic. We show that, up to bisimilarity, reasoning about Nash equilibria in multi-player non-zero-sum concurrent games can be done in ATL^* and that constructing equilibrium strategy profiles in such games can be done in 2EXPTIME using finite-memory strategies. We also study two simpler cases, two-player games and sequential games, and show that the specification of equilibria in the latter setting can be obtained in a temporal logic that is weaker than ATL^*. Based on these results, we settle a few open problems, put forward new logical characterisations of equilibria, and provide improved answers and alternative solutions to a number of questions.
Cite as

Julian Gutierrez, Paul Harrenstein, and Michael Wooldridge. Expresiveness and Complexity Results for Strategic Reasoning. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 268-282, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{gutierrez_et_al:LIPIcs.CONCUR.2015.268,
  author =	{Gutierrez, Julian and Harrenstein, Paul and Wooldridge, Michael},
  title =	{{Expresiveness and Complexity Results for Strategic Reasoning}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{268--282},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.268},
  URN =		{urn:nbn:de:0030-drops-53802},
  doi =		{10.4230/LIPIcs.CONCUR.2015.268},
  annote =	{Keywords: Temporal logic, Nash equilibrium, game models, formal verification}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact