Automatic verification of concurrent stochastic systems
From MaRDI portal
Publication:2147696
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)
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.
Recommendations
- Automated Verification of Concurrent Stochastic Games
- Multi-player equilibria verification for concurrent stochastic games
- Automatic verification of competitive stochastic systems
- Automatic verification of competitive stochastic systems
- Quantitative verification and strategy synthesis for stochastic games
Cites work
- scientific article; zbMATH DE number 5301288 (Why is no real title available?)
- scientific article; zbMATH DE number 3543391 (Why is no real title available?)
- scientific article; zbMATH DE number 3571895 (Why is no real title available?)
- scientific article; zbMATH DE number 1361118 (Why is no real title available?)
- scientific article; zbMATH DE number 700091 (Why is no real title available?)
- scientific article; zbMATH DE number 3106184 (Why is no real title available?)
- scientific article; zbMATH DE number 7649921 (Why is no real title available?)
- scientific article; zbMATH DE number 7649930 (Why is no real title available?)
- A Tool for the Automated Verification of Nash Equilibria in Concurrent Games
- A logic for reasoning about time and reliability
- A new polynomial-time algorithm for linear programming
- A survey of stochastic \(\omega \)-regular games
- Algorithmic Game Theory
- Algorithms for stochastic games ? A survey
- Alternating-time temporal logic
- Approximating values of generalized-reachability stochastic games
- Automated Verification of Concurrent Stochastic Games
- Automated temporal equilibrium analysis: verification and synthesis of multi-player games
- Automated verification and strategy synthesis for probabilistic systems
- Automatic verification of competitive stochastic systems
- Compositional strategy synthesis for stochastic games with multiple objectives
- Computer Science Logic
- Concurrent reachability games
- Enumeration of Nash equilibria for two-player games
- Equilibrium Points of Bimatrix Games
- Equilibrium points in n -person games
- Evolutionary Dynamics of Collective Action
- Interval iteration algorithm for MDPs and IMDPs
- Mixed Nash equilibria in concurrent terminal-reward games
- Model checking of probabilistic and nondeterministic systems
- Nash and correlated equilibria: Some complexity considerations
- On stochastic games with multiple objectives
- On the complexity of the parity argument and other inefficient proofs of existence
- Quantitative solution of omega-regular games
- Results on the quantitative \(\mu\)-calculus \(qM\mu\)
- Stochastic Games
- Stochastic equilibria under imprecise deviations in terminal-reward concurrent games
- Strategy improvement for concurrent reachability and turn-based stochastic safety games
- Subgame-perfect equilibria of finite- and infinite-horizon games
- The complexity of the simplex method
- The determinacy of Blackwell games
- The many facets of linear programming
- Value Iteration
- Value iteration for simple stochastic games: stopping criterion and learning algorithm
- Verification of Markov decision processes using learning algorithms
- Zermelo and the early history of game theory
Cited in
(14)- Automatic verification of competitive stochastic systems
- Automatic verification of competitive stochastic systems
- Automated temporal equilibrium analysis: verification and synthesis of multi-player games
- Automated game analysis via probabilistic model checking: a case study
- Subgame optimal strategies in finite concurrent games with prefix-independent objectives
- Multi-agent verification and control with probabilistic model checking
- Automated Verification of Concurrent Stochastic Games
- Automated Game-Theoretic Verification of Security Systems
- Symbolic verification and strategy synthesis for turn-based stochastic games
- Automatic and hierarchical verification for concurrent systems
- Correlated equilibria and fairness in concurrent stochastic games
- Equilibria-based probabilistic model checking for concurrent stochastic games
- Certified SAT solving with GPU accelerated inprocessing
- Quantitative verification and strategy synthesis for stochastic games
Describes a project that uses
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)
