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

arXiv: https://arxiv.org/abs/2405.03885 · HTML: https://mlsanity.com/paper/2405.03885/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 15 of its 47 references that are in the map.
- First posted on arXiv 6 May 2024.

## Builds on (most cited first, 15 of 15)

- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [Verification of Markov Decision Processes using Learning Algorithms](https://mlsanity.com/paper/1402.2967/) (2014)
- [TEMPEST -- Synthesis Tool for Reactive Systems and Shields in Probabilistic Environments](https://mlsanity.com/paper/2105.12588/) (2021)
- [A Practitioner's Guide to MDP Model Checking Algorithms](https://mlsanity.com/paper/2301.10197/) (2023)
- [Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm](https://mlsanity.com/paper/1804.04901/) (2018)
- [Optimistic Value Iteration](https://mlsanity.com/paper/1910.01100/) (2019)
- [Value Iteration for Long-run Average Reward in Markov Decision Processes](https://mlsanity.com/paper/1705.02326/) (2017)
- [Comparison of Algorithms for Simple Stochastic Games (Full Version)](https://mlsanity.com/paper/2008.09465/) (2020)
- [Of Cores: A Partial-Exploration Framework for Markov Decision Processes](https://mlsanity.com/paper/1906.06931/) (2019)
- [PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP](https://mlsanity.com/paper/2206.01465/) (2022)
- [Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives](https://mlsanity.com/paper/2304.09930/) (2023)
- [On Strong Determinacy of Countable Stochastic Games](https://mlsanity.com/paper/1704.05003/) (2017)
- [Anytime Guarantees for Reachability in Uncountable Markov Decision Processes](https://mlsanity.com/paper/2008.04824/) (2020)
- [Consistently faster and smaller compressed bitmaps with Roaring](https://mlsanity.com/paper/1603.06549/) (2016)
- [Optimistic and Topological Value Iteration for Simple Stochastic Games](https://mlsanity.com/paper/2207.14417/) (2022)

## Built on by (most cited first, 4 of 4)

- [Solving Robust Markov Decision Processes: Generic, Reliable, Efficient](https://mlsanity.com/paper/2412.10185/) (2024)
- [SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learning](https://mlsanity.com/paper/2501.17496/) (2025)
- [Easy-to-Use Shielding for Reinforcement Learning](https://mlsanity.com/paper/2606.03804/) (2026)
- [dtControl2+varepsilon: Trading Optimality for Explainability in MDPs via Decision Trees](https://mlsanity.com/paper/2607.25925/) (2026)

## Abstract (arXiv)

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.