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

Abstract

Abstract We present version 2.0 of thePartial Exploration Tool(Pet), a tool for verification of probabilistic systems. We extend the previous version by adding support forstochastic games, based on a recent unified framework for sound value iteration algorithms. Thereby,Pet2is 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 thatPet2offers the most efficient partial-exploration based algorithm and is the most viable tool on SGs, even outperforming unsound tools.