Playing Games with your PET: Extending the Partial Exploration Tool to Stochastic Games

TL;DR

PET2 is an advanced verification tool for stochastic games, supporting sound algorithms for reachability, safety, and mean payoff objectives, with efficient partial exploration methods outperforming existing tools.

Contribution

The paper introduces PET2, the first tool implementing sound and efficient algorithms for stochastic games with multiple objectives, including a novel partial exploration approach.

Findings

PET2 outperforms existing tools in efficiency and accuracy.

The partial exploration approach is effective for all three objectives.

PET2 is the most viable tool for stochastic game verification.

Abstract

We present version 2.0 of the Partial Exploration Tool (PET), a tool for verification of probabilistic systems. We extend the previous version by adding support for stochastic games, based on a recent unified framework for sound value iteration algorithms. Thereby, PET2 is the first tool implementing a sound and efficient approach for solving stochastic games with objectives of the type reachability/safety and mean payoff. We complement this approach by developing and implementing a partial-exploration based variant for all three objectives. Our experimental evaluation shows that PET2 offers the most efficient partial-exploration based algorithm and is the most viable tool on SGs, even outperforming unsound tools.