Automated Temporal Equilibrium Analysis: Verification and Synthesis of Multi-Player Games

• URL: http://arxiv.org/abs/2008.05638v1
• Date: Thu, 13 Aug 2020 01:43:31 GMT
• Title: Automated Temporal Equilibrium Analysis: Verification and Synthesis of Multi-Player Games
• Authors: Julian Gutierrez and Muhammad Najib and Giuseppe Perelli and Michael Wooldridge
• Abstract summary: In multi-agent systems, the rational verification problem is concerned with checking which temporal logic properties will hold in a system. We present a technique to reduce the rational verification problem to the solution of a collection of parity games.
• Score: 5.230352342979224
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In the context of multi-agent systems, the rational verification problem is concerned with checking which temporal logic properties will hold in a system when its constituent agents are assumed to behave rationally and strategically in pursuit of individual objectives. Typically, those objectives are expressed as temporal logic formulae which the relevant agent desires to see satisfied. Unfortunately, rational verification is computationally complex, and requires specialised techniques in order to obtain practically useable implementations. In this paper, we present such a technique. This technique relies on a reduction of the rational verification problem to the solution of a collection of parity games. Our approach has been implemented in the Equilibrium Verification Environment (EVE) system. The EVE system takes as input a model of a concurrent/multi-agent system represented using the Simple Reactive Modules Language (SRML), where agent goals are represented as Linear Temporal Logic (LTL) formulae, together with a claim about the equilibrium behaviour of the system, also expressed as an LTL formula. EVE can then check whether the LTL claim holds on some (or every) computation of the system that could arise through agents choosing Nash equilibrium strategies; it can also check whether a system has a Nash equilibrium, and synthesise individual strategies for players in the multi-player game. After presenting our basic framework, we describe our new technique and prove its correctness. We then describe our implementation in the EVE system, and present experimental results which show that EVE performs favourably in comparison to other existing tools that support rational verification.

Related papers

• Responsibility-aware Strategic Reasoning in Probabilistic Multi-Agent Systems [1.7819574476785418]
  Responsibility plays a key role in the development and deployment of trustworthy autonomous systems. We introduce the logic PATL+R, a variant of Probabilistic Alternating-time Temporal Logic. We present an approach to synthesise joint strategies that satisfy an outcome specified in PATL+R.
  arXiv  Detail & Related papers  (2024-10-31T18:49:12Z)
• Verified Compositional Neuro-Symbolic Control for Stochastic Systems with Temporal Logic Tasks [11.614036749291216]
  Several methods have been proposed recently to learn neural network (NN) controllers for autonomous agents. A key challenge within these approaches is that they often lack safety guarantees or the provided guarantees are impractical. This paper aims to address this challenge by checking if there exists a temporal composition of the trained NN controllers.
  arXiv  Detail & Related papers  (2023-11-17T20:51:24Z)
• On the Complexity of Rational Verification [5.230352342979224]
  Rational verification refers to the problem of checking which temporal logic properties hold of a concurrent multiagent system. We show that the complexity of rational verification can be greatly reduced by specifications. We provide improved results for rational verification when considering players' goals given by mean-payoff utility functions.
  arXiv  Detail & Related papers  (2022-07-06T12:56:22Z)
• Efficient Model-based Multi-agent Reinforcement Learning via Optimistic Equilibrium Computation [93.52573037053449]
  H-MARL (Hallucinated Multi-Agent Reinforcement Learning) learns successful equilibrium policies after a few interactions with the environment. We demonstrate our approach experimentally on an autonomous driving simulation benchmark.
  arXiv  Detail & Related papers  (2022-03-14T17:24:03Z)
• Finding General Equilibria in Many-Agent Economic Simulations Using Deep Reinforcement Learning [72.23843557783533]
  We show that deep reinforcement learning can discover stable solutions that are epsilon-Nash equilibria for a meta-game over agent types. Our approach is more flexible and does not need unrealistic assumptions, e.g., market clearing. We demonstrate our approach in real-business-cycle models, a representative family of DGE models, with 100 worker-consumers, 10 firms, and a government who taxes and redistributes.
  arXiv  Detail & Related papers  (2022-01-03T17:00:17Z)
• Automated Machine Learning, Bounded Rationality, and Rational Metareasoning [62.997667081978825]
  We will look at automated machine learning (AutoML) and related problems from the perspective of bounded rationality. Taking actions under bounded resources requires an agent to reflect on how to use these resources in an optimal way.
  arXiv  Detail & Related papers  (2021-09-10T09:10:20Z)
• Rational Verification for Probabilistic Systems [2.4254101826561847]
  We develop the theory and algorithms for rational verification in probabilistic systems. We focus on concurrent games (CSGs), which can be used to model uncertainty and randomness in complex multi-agent environments.
  arXiv  Detail & Related papers  (2021-07-19T19:24:16Z)
• Equilibrium Design for Concurrent Games [5.9873770241999]
  In game theory, mechanism design is concerned with the design of incentives so that a desired outcome of the game can be achieved. We study the design of incentives so that a desirable equilibrium is obtained, for instance, an equilibrium satisfying a given temporal logic property. As an application, equilibrium design can be used as an alternative solution to the rational synthesis and verification problems for concurrent games.
  arXiv  Detail & Related papers  (2021-06-18T15:45:45Z)
• Online Learning Probabilistic Event Calculus Theories in Answer Set Programming [70.06301658267125]
  Event Recognition (CER) systems detect occurrences in streaming time-stamped datasets using predefined event patterns. We present a system based on Answer Set Programming (ASP), capable of probabilistic reasoning with complex event patterns in the form of rules weighted in the Event Calculus. Our results demonstrate the superiority of our novel approach, both terms efficiency and predictive.
  arXiv  Detail & Related papers  (2021-03-31T23:16:29Z)
• Multi-Agent Reinforcement Learning with Temporal Logic Specifications [65.79056365594654]
  We study the problem of learning to satisfy temporal logic specifications with a group of agents in an unknown environment. We develop the first multi-agent reinforcement learning technique for temporal logic specifications. We provide correctness and convergence guarantees for our main algorithm.
  arXiv  Detail & Related papers  (2021-02-01T01:13:03Z)
• Information Freshness-Aware Task Offloading in Air-Ground Integrated Edge Computing Systems [49.80033982995667]
  This paper studies the problem of information freshness-aware task offloading in an air-ground integrated multi-access edge computing system. A third-party real-time application service provider provides computing services to the subscribed mobile users (MUs) with the limited communication and computation resources from the InP. We derive a novel deep reinforcement learning (RL) scheme that adopts two separate double deep Q-networks for each MU to approximate the Q-factor and the post-decision Q-factor.
  arXiv  Detail & Related papers  (2020-07-15T21:32:43Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.