Automatic verification of concurrent stochastic systems
From MaRDI portal
Publication:2147696
DOI10.1007/S10703-020-00356-YzbMATH Open1505.68025arXiv2008.04613OpenAlexW3124931799WikidataQ112268299 ScholiaQ112268299MaRDI QIDQ2147696FDOQ2147696
Publication date: 20 June 2022
Published in: Formal Methods in System Design (Search for Journal in Brave)
Abstract: Automated verification techniques for stochastic games allow formal reasoning about systems that feature competitive or collaborative behaviour among rational agents in uncertain or probabilistic settings. Existing tools and techniques focus on turn-based games, where each state of the game is controlled by a single player, and on zero-sum properties, where two players or coalitions have directly opposing objectives. In this paper, we present automated verification techniques for concurrent stochastic games (CSGs), which provide a more natural model of concurrent decision making and interaction. We also consider (social welfare) Nash equilibria, to formally identify scenarios where two players or coalitions with distinct goals can collaborate to optimise their joint performance. We propose an extension of the temporal logic rPATL for specifying quantitative properties in this setting and present corresponding algorithms for verification and strategy synthesis for a variant of stopping games. For finite-horizon properties the computation is exact, while for infinite-horizon it is approximate using value iteration. For zero-sum properties it requires solving matrix games via linear programming, and for equilibria-based properties we find social welfare or social cost Nash equilibria of bimatrix games via the method of labelled polytopes through an SMT encoding. We implement this approach in PRISM-games, which required extending the tool's modelling language for CSGs, and apply it to case studies from domains including robotics, computer security and computer networks, explicitly demonstrating the benefits of both CSGs and equilibria-based properties.
Full work available at URL: https://arxiv.org/abs/2008.04613
Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Specification and verification (program logics, model checking, etc.) (68Q60) Stochastic games, stochastic differential games (91A15) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- A Tool for the Automated Verification of Nash Equilibria in Concurrent Games
- A new polynomial-time algorithm for linear programming
- Algorithmic Game Theory
- Equilibrium points in n -person games
- Stochastic Games
- Alternating-time temporal logic
- Algorithms for stochastic games ? A survey
- A survey of stochastic \(\omega \)-regular games
- The determinacy of Blackwell games
- A logic for reasoning about time and reliability
- Model checking of probabilistic and nondeterministic systems
- Subgame-perfect equilibria of finite- and infinite-horizon games
- On the complexity of the parity argument and other inefficient proofs of existence
- Quantitative solution of omega-regular games
- Concurrent reachability games
- Value Iteration
- Equilibrium Points of Bimatrix Games
- Automatic verification of competitive stochastic systems
- Evolutionary Dynamics of Collective Action
- Enumeration of Nash equilibria for two-player games
- The many facets of linear programming
- Computer Science Logic
- On Stochastic Games with Multiple Objectives
- Automated Verification and Strategy Synthesis for Probabilistic Systems
- Strategy improvement for concurrent reachability and turn-based stochastic safety games
- Approximating Values of Generalized-Reachability Stochastic Games
- Zermelo and the early history of game theory
- Nash and correlated equilibria: Some complexity considerations
- Mixed Nash Equilibria in Concurrent Terminal-Reward Games
- The Complexity of the Simplex Method
- Interval iteration algorithm for MDPs and IMDPs
- Verification of Markov Decision Processes Using Learning Algorithms
- The complexity of solving reachability games using value and strategy iteration
- Compositional strategy synthesis for stochastic games with multiple objectives
- Automated temporal equilibrium analysis: verification and synthesis of multi-player games
- Automated Verification of Concurrent Stochastic Games
- Value iteration for simple stochastic games: stopping criterion and learning algorithm
- Results on the quantitative μ-calculus qM μ
Cited In (7)
- Certified SAT solving with GPU accelerated inprocessing
- Symbolic verification and strategy synthesis for turn-based stochastic games
- Subgame optimal strategies in finite concurrent games with prefix-independent objectives
- Automatic verification of competitive stochastic systems
- Correlated equilibria and fairness in concurrent stochastic games
- Automatic and hierarchical verification for concurrent systems
- Multi-agent verification and control with probabilistic model checking
Uses Software
This page was built for publication: Automatic verification of concurrent stochastic systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2147696)
