Quantitative verification and strategy synthesis for stochastic games

DOI10.1016/j.ejcon.2016.04.009zbMath1347.93240OpenAlexW2356671789MaRDI QIDQ328165

Marta Kwiatkowska, Mária Svoreňová

Publication date: 20 October 2016

Published in: European Journal of Control (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ejcon.2016.04.009

zbMATH Keywords

stochastic gamestemporal logiccontroller synthesismulti-objective propertiesquantitative verification

Mathematics Subject Classification ID

Multi-objective and goal programming (90C29) Synthesis problems (93B50) Stochastic games, stochastic differential games (91A15) Stochastic systems in control theory (general) (93E03)

Related Items (7)

Compositional strategy synthesis for stochastic games with multiple objectives ⋮ Value iteration for simple stochastic games: stopping criterion and learning algorithm ⋮ Automated Verification of Concurrent Stochastic Games ⋮ Optimistic and topological value iteration for simple stochastic games ⋮ Unnamed Item ⋮ Comparison of algorithms for simple stochastic games ⋮ Verification of multiplayer stochastic games via abstract dependency graphs

Uses Software

• GAVS
• PRISM
• PPL
• QUASY
• GIST
• PRALINE
• PRISM-games
• MOCHA
• TuLiP
• EAGLE
• MultiGain

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Compositional probabilistic verification through multi-objective model checking
• A survey of stochastic \(\omega \)-regular games
• The complexity of stochastic games
• A subexponential randomized algorithm for the simple stochastic game problem
• Optimal time-abstract schedulers for CTMDPs and continuous-time Markov games
• Continuous-time stochastic games with time-bounded reachability
• A survey of partial-observation stochastic parity games
• A Tool for the Automated Verification of Nash Equilibria in Concurrent Games
• On Stochastic Games with Multiple Objectives
• Comparison of LTL to Deterministic Rabin Automata Translators
• Multi-objective Discounted Reward Verification in Graphs and MDPs
• Automatic Verification of Competitive Stochastic Systems
• Playing Stochastic Games Precisely
• Model checking of probabilistic and nondeterministic systems
• Formal Verification and Synthesis for Discrete-Time Stochastic Systems
• Quantitative Multi-objective Verification for Probabilistic Systems
• QUASY: Quantitative Synthesis Tool
• Compositional Controller Synthesis for Stochastic Games
• The Complexity of Nash Equilibria in Stochastic Multiplayer Games
• Value Iteration
• A Pumping Algorithm for Ergodic Stochastic Mean Payoff Games with Perfect Information
• Expected Reachability-Time Games
• Reachability in Stochastic Timed Games
• The Complexity of Solving Stochastic Games on Graphs
• The Complexity of Markov Decision Processes
• The determinacy of Blackwell games
• Automated Verification and Strategy Synthesis for Probabilistic Systems
• Partial-Observation Stochastic Games
• Robust Control of Markov Decision Processes with Uncertain Transition Matrices
• PRISM-games: A Model Checker for Stochastic Multi-Player Games
• The Complexity of Partial-Observation Stochastic Parity Games with Finite-Memory Strategies
• Strategy Improvement and Randomized Subexponential Algorithms for Stochastic Parity Games
• Probabilistic automata
• Stochastic Games with Perfect Information and Time Average Payoff
• Automata, Languages and Programming
• Strategy Improvement for Stochastic Rabin and Streett Games
• Stochastic Games
• Recursive Concurrent Stochastic Games

This page was built for publication: Quantitative verification and strategy synthesis for stochastic games