Rational Verification for Probabilistic Systems

• URL: http://arxiv.org/abs/2107.09119v1
• Date: Mon, 19 Jul 2021 19:24:16 GMT
• Title: Rational Verification for Probabilistic Systems
• Authors: Julian Gutierrez, Lewis Hammond, Anthony Lin, Muhammad Najib, Michael Wooldridge
• Abstract summary: 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.
• Score: 2.4254101826561847
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: 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).

Related papers

• On Imperfect Recall in Multi-Agent Influence Diagrams [57.21088266396761]
  Multi-agent influence diagrams (MAIDs) are a popular game-theoretic model based on Bayesian networks. We show how to solve MAIDs with forgetful and absent-minded agents using mixed policies and two types of correlated equilibrium. We also describe applications of MAIDs to Markov games and team situations, where imperfect recall is often unavoidable.
  arXiv  Detail & Related papers  (2023-07-11T07:08:34Z)
• On the Complexity of Multi-Agent Decision Making: From Learning in Games to Partial Monitoring [105.13668993076801]
  A central problem in the theory of multi-agent reinforcement learning (MARL) is to understand what structural conditions and algorithmic principles lead to sample-efficient learning guarantees. We study this question in a general framework for interactive decision making with multiple agents. We show that characterizing the statistical complexity for multi-agent decision making is equivalent to characterizing the statistical complexity of single-agent decision making.
  arXiv  Detail & Related papers  (2023-05-01T06:46:22Z)
• 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)
• Finite-Sample Analysis of Decentralized Q-Learning for Stochastic Games [3.441021278275805]
  Learning in games is arguably the most standard and fundamental setting in multi-agent reinforcement learning (MARL) We establish the finite-sample complexity of fully decentralized Q-learning algorithms in a significant class of general approximation games (SGs) We focus on the practical while challenging setting of fully decentralized MARL, where neither the rewards nor the actions of other agents can be observed by each agent.
  arXiv  Detail & Related papers  (2021-12-15T03:33:39Z)
• Logical Credal Networks [87.25387518070411]
  This paper introduces Logical Credal Networks, an expressive probabilistic logic that generalizes many prior models that combine logic and probability. We investigate its performance on maximum a posteriori inference tasks, including solving Mastermind games with uncertainty and detecting credit card fraud.
  arXiv  Detail & Related papers  (2021-09-25T00:00:47Z)
• CausalCity: Complex Simulations with Agency for Causal Discovery and Reasoning [68.74447489372037]
  We present a high-fidelity simulation environment that is designed for developing algorithms for causal discovery and counterfactual reasoning. A core component of our work is to introduce textitagency, such that it is simple to define and create complex scenarios. We perform experiments with three state-of-the-art methods to create baselines and highlight the affordances of this environment.
  arXiv  Detail & Related papers  (2021-06-25T00:21:41Z)
• 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)
• Automated Temporal Equilibrium Analysis: Verification and Synthesis of Multi-Player Games [5.230352342979224]
  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.
  arXiv  Detail & Related papers  (2020-08-13T01:43:31Z)
• From Checking to Inference: Actual Causality Computations as Optimization Problems [79.87179017975235]
  We present a novel approach to formulate different notions of causal reasoning, over binary acyclic models, as optimization problems. We show that both notions are efficiently automated. Using models with more than $8000$ variables, checking is computed in a matter of seconds, with MaxSAT outperforming ILP in many cases.
  arXiv  Detail & Related papers  (2020-06-05T10:56:52Z)
• Probabilistic Performance-Pattern Decomposition (PPPD): analysis framework and applications to stochastic mechanical systems [8.975760915194765]
  The paper proposes a framework to obtain structuralized characterizations on behaviors of systems. The framework is named Probabilistic Performance-Pattern Decomposition (PPPD)
  arXiv  Detail & Related papers  (2020-03-04T17:18: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.