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.

该研究报告介绍了 Partial Exploration Tool（PET）的 2.0 版本，它是一种用于验证概率系统的工具。通过基于最近提出的统一框架的声音价值迭代算法、支持随机博弈，PET2 成为第一个实现解决类型为达到性/安全性和平均回报的随机博弈问题的声音、高效的方法的工具。此外，我们还开发并实现了基于部分探索的变体，用于处理这三种目标。我们的实验评估表明，PET2 提供了最有效的基于部分探索的算法，并成为了在随机博弈中最可行的工具，甚至优于不完备的工具。

与你的宠物玩游戏：将部分探索工具扩展到随机博弈