PRISM-games 3.0: Stochastic game verification with concurrency, equilibria and time by Kwiatkowska, M, Norman, G, Parker, D, Santos, G

“…We present a major new release of the PRISM-games model checker, featuring multiple significant advances in its support for verification and strategy synthesis of stochastic games. …”

PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives by Kwiatkowska, M, Parker, D, Wiltsche, C

“…PRISM-games is a tool for modelling, verification and strategy synthesis for stochastic multi-player games. …”

PLAYING STOCHASTIC GAMES PRECISELY by Chen, T, Forejt, V, Kwiatkowska, M, Simaitis, A, Trivedi, A, Ummels, M

“…We study stochastic two-player games where the goal of one player is to achieve precisely a given expected value of the objective function, while the goal of the opponent is the opposite. …”

Expected reachability-time games by Forejt, V, Kwiatkowska, M, Norman, G, Trivedi, A

“…We study two-player zero-sum games on such automata where the objective of the game is specified as the expected time to reach a target. …”

Expected Reachability−Time Games by Forejt, V, Kwiatkowska, M, Norman, G, Trivedi, A

Playing Stochastic Games Precisely by Chen, T, Forejt, V, Kwiatkowska, M, Simaitis, A, Trivedi, A, Ummels, M

On Stochastic Games with Multiple Objectives by Chen, T, Forejt, V, Kwiatkowska, M, Simaitis, A, Wiltsche, C

“…Such games are important for modelling, synthesis and veri cation of open systems with stochastic behaviour. …”

Expected Reachability-Time Games. by Forejt, V, Kwiatkowska, M, Norman, G, Trivedi, A

“…These games are concurrent since at each step of the game both players choose a timed move (a time delay and action under their control), and the transition of the game is determined by the timed move of the player who proposes the shorter delay. …”

PRISM-games 2.0: a tool for multi-objective strategy synthesis for stochastic games by Kwiatkowska, M, Wiltsche, C, Parker, D

“…We present a new release of PRISM-games, a tool for veri- fication and strategy synthesis for stochastic games. …”

Automated verification of concurrent stochastic games by Kwiatkowska, M, Norman, G, Parker, D, Santos, G

“…We present automatic verification techniques for concurrent stochastic multi-player games (CSGs) with rewards. To express properties of such models, we adapt the temporal logic rPATL (probabilistic alternating-time temporal logic with rewards), originally introduced for the simpler model of turn-based games, which enables quantitative reasoning about the ability of coalitions of players to achieve goals related to the probability of an event or reward measures. …”

Compositional Controller Synthesis for Stochastic Games by Basset, N, Kwiatkowska, M, Wiltsche, C

“…We propose a synchronising parallel composition for stochastic games that enables a compositional approach to controller synthesis. …”

Correlated equilibria and fairness in concurrent stochastic games by Kwiatkowska, M, Norman, G, Parker, D, Santos, G

“…Game-theoretic techniques and equilibria analysis facilitate the design and verification of competitive systems. …”

Quantitative verification and strategy synthesis of stochastic games by Svorenova, M, Kwiatkowska, M

“…In this paper, we focus on analysis of complex computer systems modelled as turn-based 21/2-player games, or stochastic games for short, that are able to express both stochastic and non-stochastic uncertainty. …”

Game−Based Probabilistic Predicate Abstraction in PRISM by Kattenbelt, M, Kwiatkowska, M, Norman, G, Parker, D

Game−Based Probabilistic Predicate Abstraction in PRISM by Kattenbelt, M, Kwiatkowska, M, Norman, G, Parker, D

Assume-guarantee strategy synthesis for stochastic games by Wiltsche, C

“…We model systems as turn-based two-player zero-sum stochastic games, which are able to express both stochastic and nondeterministic environmental uncertainty. …”

Multi-player equilibria verification for concurrent stochastic games by Kwiatkowska, M, Norman, G, Parker, D, Santos, G

“…Concurrent stochastic games (CSGs) are an ideal formalism for modelling probabilistic systems that feature multiple players or components with distinct objectives making concurrent, rational decisions. …”

Compositional strategy synthesis for stochastic games with multiple objectives by Basset, N, Kwiatkowska, M, Wiltsche, C

“…We then develop an algorithm to synthesise ε-optimal strategies for conjunctions of almost sure satisfaction for mean payoffs and ratio rewards (in general games) and Boolean combinations of expected mean-payoffs (in controllable multi-chain games). …”

Partially observable stochastic games with neural perception mechanisms by Yan, R, Santos, G, Norman, G, Parker, D, Kwiatkowska, M

“…Stochastic games are a well established model for multi-agent sequential decision making under uncertainty. …”

Verification and control of turn-based probabilistic real-time games by Kwiatkowska, M, Norman, G, Parker, D

“…We propose the model of turn-based probabilistic timed multi-player games, which incorporates probabilistic choice, real-time clocks and nondeterministic behaviour across multiple players. …”