Add PRISM-games plugin for probabilistic model checking on stochastic games

[elazarg]

Summary

Add a PRISM-games plugin to enable probabilistic model checking and temporal-logic queries on stochastic multi-player games — a capability axis not covered by any existing plugin.

Motivation

Current plugins cover:

Plugin	Coverage
gambit	Classical NE / strategic & extensive form
pycid	Causal influence diagrams
vegas	Vegas DSL
egttools	Evolutionary dynamics
openspiel	CFR, exploitability

None handle probabilistic verification of games — i.e. answering questions like "can coalition C ensure property P with probability ≥ 0.9?" on a stochastic multi-player game.

PRISM-games (Oxford/Birmingham, actively maintained, v3.2.x) adds:

• Turn-based and concurrent stochastic games (CSGs)
• rPATL / rPATL* temporal-logic queries (reachability, expected reward, ratio rewards, …)
• Nash and social-welfare equilibria for CSGs
• Real-time models (probabilistic timed games)

This is a meaningful new analysis family, not a duplicate of existing tools.

Integration sketch

Fits the existing remote-plugin contract (/health, /info, /analyze, /parse/{format}):

• Container: JRE + PRISM-games release; FastAPI wrapper invoking the prism CLI via subprocess and parsing result files.
• New format: .prism (PRISM-games modelling language) registered as a parser. Not convertible from .efg/.nfg — PRISM models are their own family.
• Analyses: parametric over a property string (rPATL formula) plus optional constants; return value/strategy/equilibrium payload.
• Port: e.g. 5006, matching the table in CLAUDE.md.

Costs / caveats

• License: GPL v2. Other plugins are mostly permissive. Running PRISM-games as a separate HTTP service keeps us out of derivative-work territory, but it is a conscious choice worth recording.
• Heavy image (JRE + PRISM + native libs, hundreds of MB) and slower startup — fits the existing startup_timeout_seconds knob.
• No shared input format with existing games — does not enrich analyses on .efg/.nfg/JSON inputs; adds a parallel game family.
• No native Python API — integration is via CLI, so output parsing is the main correctness risk.

Scope for a first cut

• plugins/prism/ service: Dockerfile (JRE + PRISM-games), FastAPI wrapper
• /parse/prism for .prism input
• One analysis: rPATL property check (value + optimal strategy if available)
• One analysis: CSG equilibrium (Nash / social-welfare) on a CSG model
• Health check + plugin registration in plugins.toml / docker-compose.yml
• One example model in examples/
• Integration test exercising parse → analyze

References

• https://www.prismmodelchecker.org/games/
• https://github.com/prismmodelchecker/prism-games
• PRISM-games 3.0 (TACAS 2020): https://link.springer.com/chapter/10.1007/978-3-030-53291-8_25