GIST: A Solver for Probabilistic Games

TL;DR

GIST is a tool that efficiently solves probabilistic games with complex objectives and synthesizes environment assumptions for unrealizable specifications, advancing analysis and synthesis in probabilistic systems.

Contribution

It provides the first efficient implementation of reduction techniques for solving turn-based probabilistic games and uses this analysis for environment assumption synthesis.

Findings

First efficient implementation of reduction-based techniques

Solves qualitative analysis of probabilistic games

Synthesizes environment assumptions for unrealizable specs

Abstract

Gist is a tool that (a) solves the qualitative analysis problem of turn-based probabilistic games with {\omega}-regular objectives; and (b) synthesizes reasonable environment assumptions for synthesis of unrealizable specifications. Our tool provides the first and efficient implementations of several reduction-based techniques to solve turn-based probabilistic games, and uses the analysis of turn-based probabilistic games for synthesizing environment assumptions for unrealizable specifications.