On the Complexity of Rational Verification

• URL: http://arxiv.org/abs/2207.02637v1
• Date: Wed, 6 Jul 2022 12:56:22 GMT
• Title: On the Complexity of Rational Verification
• Authors: Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, Michael Wooldridge
• Abstract summary: 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.
• Score: 5.230352342979224
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Rational verification refers to the problem of checking which temporal logic properties hold of a concurrent multiagent system, under the assumption that agents in the system choose strategies that form a game-theoretic equilibrium. Rational verification can be understood as a counterpart to model checking for multiagent systems, but while classical 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 harder: the key decision problems for rational verification are 2EXPTIME-complete with LTL specifications, even when using explicit-state system representations. Against this background, our contributions in this paper are threefold. First, 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 a broad and practically useful class of response properties of reactive systems. In particular, we show that for a number of relevant settings, rational verification can be done in polynomial space and even in polynomial time. Second, we provide improved complexity results for rational verification when considering players' goals given by mean-payoff utility functions; arguably the most widely used approach for quantitative objectives in concurrent and multiagent systems. Finally, we consider the problem of computing outcomes that satisfy social welfare constraints. To this end, we consider both utilitarian and egalitarian social welfare and show that computing such outcomes is either PSPACE-complete or NP-complete.

Related papers

• Optimal Control of Logically Constrained Partially Observable and Multi-Agent Markov Decision Processes [5.471640959988549]
  We first introduce an optimal control theory for partially observable Markov decision processes. We provide a structured methodology for synthesizing policies that maximize a cumulative reward. We then build on this approach to design an optimal control framework for logically constrained multi-agent settings.
  arXiv  Detail & Related papers  (2023-05-24T05:15:36Z)
• Efficient Knowledge Compilation Beyond Weighted Model Counting [7.828647825246474]
  We introduce Second Level Algebraic Model Counting (2AMC) as a generic framework for these kinds of problems. First level techniques based on Knowledge Compilation (KC) have been adapted for specific 2AMC instances by imposing variable order constraints. We show that we can exploit the logical structure of a 2AMC problem to omit parts of these constraints, thus limiting the negative effect.
  arXiv  Detail & Related papers  (2022-05-16T08:10:40Z)
• Logical blocks for fault-tolerant topological quantum computation [55.41644538483948]
  We present a framework for universal fault-tolerant logic motivated by the need for platform-independent logical gate definitions. We explore novel schemes for universal logic that improve resource overheads. Motivated by the favorable logical error rates for boundaryless computation, we introduce a novel computational scheme.
  arXiv  Detail & Related papers  (2021-12-22T19:00:03Z)
• 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)
• 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)
• Joint Contrastive Learning with Infinite Possibilities [114.45811348666898]
  This paper explores useful modifications of the recent development in contrastive learning via novel probabilistic modeling. We derive a particular form of contrastive loss named Joint Contrastive Learning (JCL)
  arXiv  Detail & Related papers  (2020-09-30T16:24:21Z)
• 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)
• On Sufficient and Necessary Conditions in Bounded CTL: A Forgetting Approach [3.9461038686072847]
  We introduce a forgetting-based approach in Computation Tree Logic (CTL) We show that it can be used to compute the strongest necessary condition (SNC) and the weakest sufficient condition (WSC) of a property under a given model and over a given signature. We also study its theoretical properties and show that our notion of forgetting satisfies existing essential postulates of knowledge forgetting.
  arXiv  Detail & Related papers  (2020-03-13T21:51:59Z)
• Public Bayesian Persuasion: Being Almost Optimal and Almost Persuasive [57.47546090379434]
  We study the public persuasion problem in the general setting with: (i) arbitrary state spaces; (ii) arbitrary action spaces; (iii) arbitrary sender's utility functions. We provide a quasi-polynomial time bi-criteria approximation algorithm for arbitrary public persuasion problems that, in specific settings, yields a QPTAS.
  arXiv  Detail & Related papers  (2020-02-12T18:59:18Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  We propose a model-free RL algorithm that enables the use of Linear Temporal Logic (LTL) to formulate a goal for unknown continuous-state/action Markov Decision Processes (MDPs) The algorithm is guaranteed to synthesise a control policy whose traces satisfy the specification with maximal probability.
  arXiv  Detail & Related papers  (2019-02-02T20:09:32Z)

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.