Robust Verification of Concurrent Stochastic Games

• URL: http://arxiv.org/abs/2601.12003v2
• Date: Wed, 21 Jan 2026 09:31:07 GMT
• Title: Robust Verification of Concurrent Stochastic Games
• Authors: Angel Y. He, David Parker,
• Abstract summary: We introduce *robust CSGs* and their subclass *interval CSGs* (ICSGs)<n>We propose a novel framework for *robust* verification of these models under worst-case assumptions about transition uncertainty.<n>We build an implementation in the PRISMgames model checker and demonstrate the feasibility of robust verification of ICSGs across a selection of large benchmarks.
• Score: 3.2964666213105587
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Autonomous systems often operate in multi-agent settings and need to make concurrent, strategic decisions, typically in uncertain environments. Verification and control problems for these systems can be tackled with concurrent stochastic games (CSGs), but this model requires transition probabilities to be precisely specified - an unrealistic requirement in many real-world settings. We introduce *robust CSGs* and their subclass *interval CSGs* (ICSGs), which capture epistemic uncertainty about transition probabilities in CSGs. We propose a novel framework for *robust* verification of these models under worst-case assumptions about transition uncertainty. Specifically, we develop the underlying theoretical foundations and efficient algorithms, for finite- and infinite-horizon objectives in both zero-sum and nonzero-sum settings, the latter based on (social-welfare optimal) Nash equilibria. We build an implementation in the PRISM-games model checker and demonstrate the feasibility of robust verification of ICSGs across a selection of large benchmarks.

Related papers

• SURE: Semi-dense Uncertainty-REfined Feature Matching [28.68008638977835]
  SURE is a Semi- dense Uncertainty-REfined matching framework that jointly predicts correspondences and their confidence.<n>Our approach in- troduces a novel evidential head for trustworthy coordinate regression, along with a lightweight spatial fusion module.<n>Our method consistently outperforms existing state-of-the-art semi-dense matching models in both accuracy and efficiency.
  arXiv  Detail & Related papers  (2026-03-05T06:53:11Z)
• GTS: Inference-Time Scaling of Latent Reasoning with a Learnable Gaussian Thought Sampler [54.10960908347221]
  We model latent thought exploration as conditional sampling from learnable densities and instantiate this idea as a Gaussian Thought Sampler (GTS)<n>GTS predicts context-dependent perturbation distributions over continuous reasoning states and is trained with GRPO-style policy optimization while keeping the backbone frozen.
  arXiv  Detail & Related papers  (2026-02-15T09:57:47Z)
• CreditAudit: 2$^\ ext{nd}$ Dimension for LLM Evaluation and Selection [44.251742023911135]
  CreditAudit is a deployment oriented credit audit framework that evaluates models under a family of semantically aligned and non adversarial system prompt templates.<n>We show that models with similar mean ability can exhibit substantially different fluctuation, and stability risk can overturn prioritization decisions in agentic or high failure cost regimes.
  arXiv  Detail & Related papers  (2026-01-23T07:53:25Z)
• A Statistical Side-Channel Risk Model for Timing Variability in Lattice-Based Post-Quantum Cryptography [0.0]
  Timing side-channels are an important threat to cryptography that still needs to be addressed in implementations.<n> lattice-based schemes may produce secret-dependent timing variability with the help of complex arithmetic and control flow.<n>A scenario-based statistical risk model is proposed for timing leakage as a problem of distributional distinguishability under controlled execution conditions.
  arXiv  Detail & Related papers  (2025-12-26T03:12:33Z)
• NDCG-Consistent Softmax Approximation with Accelerated Convergence [67.10365329542365]
  We propose novel loss formulations that align directly with ranking metrics.<n>We integrate the proposed RG losses with the highly efficient Alternating Least Squares (ALS) optimization method.<n> Empirical evaluations on real-world datasets demonstrate that our approach achieves comparable or superior ranking performance.
  arXiv  Detail & Related papers  (2025-06-11T06:59:17Z)
• Automatically Adaptive Conformal Risk Control [49.95190019041905]
  We propose a methodology for achieving approximate conditional control of statistical risks by adapting to the difficulty of test samples.<n>Our framework goes beyond traditional conditional risk control based on user-provided conditioning events to the algorithmic, data-driven determination of appropriate function classes for conditioning.
  arXiv  Detail & Related papers  (2024-06-25T08:29:32Z)
• LLM4Rerank: LLM-based Auto-Reranking Framework for Recommendations [51.76373105981212]
  Reranking is a critical component in recommender systems, playing an essential role in refining the output of recommendation algorithms.<n>We introduce a comprehensive reranking framework, designed to seamlessly integrate various reranking criteria.<n>A customizable input mechanism is also integrated, enabling the tuning of the language model's focus to meet specific reranking needs.
  arXiv  Detail & Related papers  (2024-06-18T09:29:18Z)
• Asynchronous Federated Learning with Incentive Mechanism Based on Contract Theory [5.502596101979607]
  We propose a novel asynchronous FL framework that integrates an incentive mechanism based on contract theory. Our framework exhibits a 1.35% accuracy improvement over the ideal Local SGD under attacks.
  arXiv  Detail & Related papers  (2023-10-10T09:17:17Z)
• Calibrated Stackelberg Games: Learning Optimal Commitments Against Calibrated Agents [15.145023509806977]
  Calibrated Stackelberg Games (CSGs) is a new type of Stackelberg Games (SGs) In CSGs, a principal repeatedly interacts with an agent who (contrary to standard SGs) does not have direct access to the principal's action but instead best-responds to calibrated forecasts about it. We show that in CSGs, the principal can achieve utility that converges to the optimum Stackelberg value of the game both in finite and continuous settings.
  arXiv  Detail & Related papers  (2023-06-05T08:55:50Z)
• 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)
• Stochastic Gradient Descent-Ascent and Consensus Optimization for Smooth Games: Convergence Analysis under Expected Co-coercivity [49.66890309455787]
  We introduce the expected co-coercivity condition, explain its benefits, and provide the first last-iterate convergence guarantees of SGDA and SCO. We prove linear convergence of both methods to a neighborhood of the solution when they use constant step-size. Our convergence guarantees hold under the arbitrary sampling paradigm, and we give insights into the complexity of minibatching.
  arXiv  Detail & Related papers  (2021-06-30T18:32:46Z)
• Pointwise Feasibility of Gaussian Process-based Safety-Critical Control under Model Uncertainty [77.18483084440182]
  Control Barrier Functions (CBFs) and Control Lyapunov Functions (CLFs) are popular tools for enforcing safety and stability of a controlled system, respectively. We present a Gaussian Process (GP)-based approach to tackle the problem of model uncertainty in safety-critical controllers that use CBFs and CLFs.
  arXiv  Detail & Related papers  (2021-06-13T23:08:49Z)

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.