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

TL;DR

Stochastic games extend verification to two-player decision problems under uncertainty and require sound value-iteration methods. The authors introduce PET2, the first tool to provide sound and efficient VI-based solutions for SGs with reachability/safety and mean payoff objectives, featuring CE and PE variants grounded in a unified framework from lics23. Empirical results demonstrate PET2's soundness, scalability, and competitive performance, often outperforming unsound SG tools like Prism-games and Tempest while matching Pet1's capabilities. The work advances practical SG verification and points to future enhancements such as total reward support and adaptive parameterization.

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.

Figures (4)

• Figure 1: Example SGs to explain deflating and inflating. States with upward and downward triangles denote Maximizer and Minimizer states, respectively.
• Figure 2: Comparison of Pet2 to other tools. From left to right we compare Pet2-PE and Pet1-PE, Pet2-CE on MDP and MC with Storm () and Prism-games (), and finally Pet2-CE on SG with Tempest (), Prism-games (), and Prism-ext (). A point $(x, y)$ denotes that tool X and Pet2 needed $x$ and $y$ seconds, respectively. If a point is above/below the diagonal, tool X is faster/slower. Plots are on logarithmic scale, dashed diagonals indicate that one tool is twice as fast. Timeouts are pushed to the orthogonal dashed line.
• Figure 3: Example MDP to show the error in the guidance heuristic of EKKW22.
• Figure 4: Further comparisons of Pet2 to other tools. From left to right, top to bottom, we compare Pet2-CE and Pet1-CE, Pet2-CE and Pet2-PE, Pet2-PE and Storm-PE, Pet2-CE and Prism-games () / Storm () with hybrid engine, Pet2-CE with mean payoff from reachability and Prism-games, and Pet2-CE with mean payoff from reachability with Pet2-CE. We use the same graph presentation as in \ref{['fig:results']}.