mlsanityData to 14 Oct 2026

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

arXiv 2405.03885 ↗First posted 6 May 2024eess.SY cs.AI cs.GTcited by 4

Not on the map. Why?

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.

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

15 of 47 references.

References · 15

  1. 2020The Probabilistic Model Checker Stormcited by 66
  2. 2014Verification of Markov Decision Processes using Learning Algorithmscited by 39
  3. 2021TEMPEST -- Synthesis Tool for Reactive Systems and Shields in Probabilistic Environmentscited by 13
  4. 2023A Practitioner's Guide to MDP Model Checking Algorithmscited by 10
  5. 2018Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithmcited by 8
  6. 2019Optimistic Value Iterationcited by 8
  7. 2017Value Iteration for Long-run Average Reward in Markov Decision Processescited by 7
  8. 2020Comparison of Algorithms for Simple Stochastic Games (Full Version)cited by 5
  9. 2019Of Cores: A Partial-Exploration Framework for Markov Decision Processescited by 4
  10. 2022PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDPcited by 4
  11. 2023Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectivescited by 3
  12. 2017On Strong Determinacy of Countable Stochastic Gamescited by 2
3 more
  1. 2020Anytime Guarantees for Reachability in Uncountable Markov Decision Processescited by 2
  2. 2016Consistently faster and smaller compressed bitmaps with Roaringcited by 1
  3. 2022Optimistic and Topological Value Iteration for Simple Stochastic Gamescited by 1

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2024: 1; 2025: 1; 2026: 2.

4 papers.

  1. 2024Solving Robust Markov Decision Processes: Generic, Reliable, Efficientcited by 11
  2. 2025SemML: Enhancing Automata-Theoretic LTL Synthesis with Machine Learningcited by 6
  3. 2026Easy-to-Use Shielding for Reinforcement Learningcited by 1
  4. 2026dtControl2+varepsilon: Trading Optimality for Explainability in MDPs via Decision Treescited by 0