Search Results

Documents authored by Wooldridge, Michael J.

Found 2 Possible Name Variants:

Wooldridge, Michael J.

Document
DOI: 10.4230/DagRep.7.3.27
Game Theory in AI, Logic, and Algorithms (Dagstuhl Seminar 17111)

Authors: Swarat Chaudhuri, Sampath Kannan, Rupak Majumdar, and Michael J. Wooldridge

Published in: Dagstuhl Reports, Volume 7, Issue 3 (2017)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 17111 "Game Theory in AI, Logic, and Algorithms".
Cite as

Swarat Chaudhuri, Sampath Kannan, Rupak Majumdar, and Michael J. Wooldridge. Game Theory in AI, Logic, and Algorithms (Dagstuhl Seminar 17111). In Dagstuhl Reports, Volume 7, Issue 3, pp. 27-32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{chaudhuri_et_al:DagRep.7.3.27,
  author =	{Chaudhuri, Swarat and Kannan, Sampath and Majumdar, Rupak and Wooldridge, Michael J.},
  title =	{{Game Theory in AI, Logic, and Algorithms (Dagstuhl Seminar 17111)}},
  pages =	{27--32},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2017},
  volume =	{7},
  number =	{3},
  editor =	{Chaudhuri, Swarat and Kannan, Sampath and Majumdar, Rupak and Wooldridge, Michael J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.7.3.27},
  URN =		{urn:nbn:de:0030-drops-79609},
  doi =		{10.4230/DagRep.7.3.27},
  annote =	{Keywords: game theory, formal methods, logic, algorithms, equilibria, multiagent systems}
}
Document
DOI: 10.4230/DagSemRep.331
The Logic of Rational Agency (Dagstuhl Seminar 02041)

Authors: Wiebe van der Hoek and Michael J. Wooldridge

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Wiebe van der Hoek and Michael J. Wooldridge. The Logic of Rational Agency (Dagstuhl Seminar 02041). Dagstuhl Seminar Report 331, pp. 1-11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2003)

Copy BibTex To Clipboard

@TechReport{vanderhoek_et_al:DagSemRep.331,
  author =	{van der Hoek, Wiebe and Wooldridge, Michael J.},
  title =	{{The Logic of Rational Agency (Dagstuhl Seminar 02041)}},
  pages =	{1--11},
  ISSN =	{1619-0203},
  year =	{2003},
  type = 	{Dagstuhl Seminar Report},
  number =	{331},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.331},
  URN =		{urn:nbn:de:0030-drops-152140},
  doi =		{10.4230/DagSemRep.331},
}

Wooldridge, Michael

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}
}
Document
DOI: 10.4230/DagSemProc.09121.27
Robust Normative Systems

Authors: Thomas Agotnes, Wiebe van der Hoek, and Michael Wooldridge

Published in: Dagstuhl Seminar Proceedings, Volume 9121, Normative Multi-Agent Systems (2009)

Abstract
Although normative systems, or social laws, have proved to be a highly influential approach to coordination in multi-agent systems, the issue of emph{compliance} to such normative systems remains problematic. In all real systems, it is possible that some members of an agent population will not comply with the rules of a normative system, even if it is in their interests to do so. It is therefore important to consider the extent to which a normative system is emph{robust}, i.e., the extent to which it remains effective even if some agents do not comply with it. We formalise and investigate three different notions of robustness and related decision problems. We begin by considering sets of agents whose compliance is necessary and/or sufficient to guarantee the effectiveness of a normative system; we then consider quantitative approaches to robustness, where we try to identify the proportion of an agent population that must comply in order to ensure success, and finally, we consider a more general approach, where we characterise the compliance conditions required for success as a logical formula.
Cite as

Thomas Agotnes, Wiebe van der Hoek, and Michael Wooldridge. Robust Normative Systems. In Normative Multi-Agent Systems. Dagstuhl Seminar Proceedings, Volume 9121, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{agotnes_et_al:DagSemProc.09121.27,
  author =	{Agotnes, Thomas and van der Hoek, Wiebe and Wooldridge, Michael},
  title =	{{Robust Normative Systems}},
  booktitle =	{Normative Multi-Agent Systems},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9121},
  editor =	{Guido Boella and Pablo Noriega and Gabriella Pigozzi and Harko Verhagen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09121.27},
  URN =		{urn:nbn:de:0030-drops-18971},
  doi =		{10.4230/DagSemProc.09121.27},
  annote =	{Keywords: Normative systems, robustness, fault tolerance, complexity}
}
Document
DOI: 10.4230/DagSemProc.07122.24
On the Logic of Normative Systems

Authors: Thomas Ågotnes, Wiebe van der Hoek, Juan A. Rodriguez-Aguilar, Carles Sierra, and Michael Wooldridge

Published in: Dagstuhl Seminar Proceedings, Volume 7122, Normative Multi-agent Systems (2007)

Abstract
We introduce emph{Normative Temporal Logic} (acro{ntl}), a logic for reasoning about normative systems. acro{ntl} is a generalisation of the well-known branching-time temporal logic acro{ctl}, in which the path quantifiers $Apath$ (``on all pathsldots'') and $Epath$ (``on some pathldots'') are replaced by the indexed deontic operators $O{ s}$ and $P{ s}$, where for example $O{ s}phi$ means ``$phi$ is obligatory in the context of normative system $ s$''. After defining the logic, we give a sound and complete axiomatisation, and discuss the logic's relationship to standard deontic logics. We present a symbolic representation language for models and normative systems, and identify four different model checking problems, corresponding to whether or not a model is represented symbolically or explicitly, and whether or not we are given an interpretation for the normative systems named in formulae to be checked. We show that the complexity of model checking varies from acro{p}-complete up to acro{exptime}-hard for these variations.
Cite as

Thomas Ågotnes, Wiebe van der Hoek, Juan A. Rodriguez-Aguilar, Carles Sierra, and Michael Wooldridge. On the Logic of Normative Systems. In Normative Multi-agent Systems. Dagstuhl Seminar Proceedings, Volume 7122, pp. 1-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{agotnes_et_al:DagSemProc.07122.24,
  author =	{\r{A}gotnes, Thomas and van der Hoek, Wiebe and Rodriguez-Aguilar, Juan A. and Sierra, Carles and Wooldridge, Michael},
  title =	{{On the Logic of Normative Systems}},
  booktitle =	{Normative Multi-agent Systems},
  pages =	{1--13},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7122},
  editor =	{Guido Boella and Leon van der Torre and Harko Verhagen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07122.24},
  URN =		{urn:nbn:de:0030-drops-9210},
  doi =		{10.4230/DagSemProc.07122.24},
  annote =	{Keywords: Normative systems, normative temporal logic, deontic logic}
}
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 About DROPS Imprint Privacy Contact