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
• 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

• Monitoring Data-aware Temporal Properties (Extended Version) [56.386411908764494]
  We consider anticipatory monitoring of linear-time properties enriched with an arbitrary SMT theory over finite traces.<n>Anticipatory monitoring in this setting is highly challenging, as the monitoring state depends on both the trace prefix seen so far and all its possible finite continuations.<n>We present and formally prove the correctness of a novel foundational framework for monitoring properties in an expressive fragment offMT.
  arXiv  Detail & Related papers  (2026-05-14T10:23:11Z)
• SGA-MCTS: Decoupling Planning from Execution via Training-Free Atomic Experience Retrieval [74.1918709002557]
  We introduce textbfSGA-MCTS, a framework that casts LLM planning as non-parametric retrieval.<n>Online, a retrieval-augmented agent employs a hybrid symbolic-semantic mechanism to fetch relevant State-Goal-Action atoms.<n>By effectively amortizing the heavy computational cost of search, SGA-MCTS achieves System 2 reasoning depth at System 1 inference speeds, rendering autonomous planning both scalable and real-time feasible.
  arXiv  Detail & Related papers  (2026-04-16T07:22:36Z)
• Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version) [49.462399222747024]
  We propose a novel framework for the logical specification of non-Markovian rewards in Decision Processes (MDPs) with large state spaces.<n>Our approach leverages Linear Temporal Logic Modulo Theories over finite traces (LTLfMT)<n>We introduce a method based on reward machines and Hindsight Experience Replay (HER) to translate first-order logic specifications and address reward sparsity.
  arXiv  Detail & Related papers  (2026-02-05T22:11:28Z)
• OrLog: Resolving Complex Queries with LLMs and Probabilistic Reasoning [51.58235452818926]
  We introduce OrLog, a neuro-symbolic retrieval framework that decouples predicate-level plausibility estimation from logical reasoning.<n>A large language model (LLM) provides plausibility scores for atomic predicates in one decoding-free forward pass, from which a probabilistic reasoning engine derives the posterior probability of query satisfaction.
  arXiv  Detail & Related papers  (2026-01-30T15:31:58Z)
• CoT-Seg: Rethinking Segmentation with Chain-of-Thought Reasoning and Self-Correction [50.67483317563736]
  This paper aims to explore a system that can think step-by-step, look up information if needed, generate results, self-evaluate its own results, and refine the results.<n>We introduce CoT-Seg, a training-free framework that rethinks reasoning segmentation by combining chain-of-thought reasoning with self-correction.
  arXiv  Detail & Related papers  (2026-01-24T11:41:54Z)
• Benefits and Limitations of Communication in Multi-Agent Reasoning [11.788489289062312]
  We propose a theoretical framework to analyze the expressivity of multi-agent systems.<n>We derive bounds on (i) the number of agents required to solve the task exactly, (ii) the quantity and structure of inter-agent communication, and (iii) the achievable speedups as problem size and context scale.<n>Our results identify regimes where communication is provably beneficial, delineate tradeoffs between agent count and bandwidth, and expose intrinsic limitations when either resource is constrained.
  arXiv  Detail & Related papers  (2025-10-14T20:04:27Z)
• seqBench: A Tunable Benchmark to Quantify Sequential Reasoning Limits of LLMs [1.0519693622157462]
  We introduce seqBench, a benchmark for probing sequential reasoning limits in Large Language Models (LLMs)<n>We find that even top-performing models systematically fail on seqBench's structured reasoning tasks despite minimal search complexity.
  arXiv  Detail & Related papers  (2025-09-21T01:32:13Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  We develop CompassVerifier, an accurate and robust lightweight verifier model for evaluation and outcome reward.<n>It demonstrates multi-domain competency spanning math, knowledge, and diverse reasoning tasks, with the capability to process various answer types.<n>We introduce VerifierBench benchmark comprising model outputs collected from multiple data sources, augmented through manual analysis of metaerror patterns to enhance CompassVerifier.
  arXiv  Detail & Related papers  (2025-08-05T17:55:24Z)
• T-CPDL: A Temporal Causal Probabilistic Description Logic for Developing Logic-RAG Agent [5.439020425819001]
  Temporal Causal Probabilistic Description Logic (T-CPDL) is an integrated framework that extends Description Logic with temporal interval operators, explicit causal relationships, and probabilistic annotations.<n>T-CPDL substantially improves inference accuracy, interpretability, and confidence calibration of language model outputs.<n>This work also lays the groundwork for developing advanced Logic-Retrieval-Augmented Generation (Logic-RAG) frameworks.
  arXiv  Detail & Related papers  (2025-06-23T12:11:15Z)
• PixelThink: Towards Efficient Chain-of-Pixel Reasoning [70.32510083790069]
  PixelThink is a simple yet effective scheme that integrates externally estimated task difficulty and internally measured model uncertainty.<n>It learns to compress reasoning length in accordance with scene complexity and predictive confidence.<n> Experimental results demonstrate that the proposed approach improves both reasoning efficiency and overall segmentation performance.
  arXiv  Detail & Related papers  (2025-05-29T17:55:49Z)
• Critical Thinking: Which Kinds of Complexity Govern Optimal Reasoning Length? [72.70486097967124]
  We formalize a framework using deterministic finite automata (DFAs) We show that there exists an optimal amount of reasoning tokens such that the probability of producing a correct solution is maximized. We then demonstrate an implication of these findings: being able to predict the optimal number of reasoning tokens for new problems and filtering out non-optimal length answers results in consistent accuracy improvements.
  arXiv  Detail & Related papers  (2025-04-02T17:45:58Z)
• Time-optimal neural feedback control of nilpotent systems as a binary classification problem [0.6999740786886538]
  computational method for synthesis of time-optimal feedback control laws. System is sampled and solved to generate a dataset for the construction of a time-optimal deep neural network. Tests assess the accuracy, robustness, and real-time-control capabilities of the approximate control law.
  arXiv  Detail & Related papers  (2025-03-21T23:36:20Z)
• 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.