On this page
Mean payoff strategy synthesis plugin
Edition: 8 October 2026. Initial decision: Conditional engineering. The product interpretation and pricing are hypotheses; independent proof and buyer validation remain open.
Research finding
The family claims quasipolynomial algorithms for several signed-weight mean-payoff and parity-game variants. Its scope notes formalize a randomized zero-threshold mean-payoff algorithm and a finite counterexample, rather than all newer deterministic and stochastic extensions.
Problem and buyer
A formal-methods team can model repeated resource or adversarial decisions as finite games, then needs values, winning states or strategies under precisely stated payoff semantics.
What the finding could enable
A backend plugin could broaden practical game solving if it handles binary reward encodings more effectively than existing methods. It can support formal modeling workflows without claiming that an informal business process has been fully verified.
Technical and commercial limits
Ordinary exact values, stochastic threshold sets and parity-conjoined winning sets are different outputs. Model extraction and objective semantics are major risks. Quasipolynomial time can still be impractical.
Minimal architecture
Game-format adapter -> payoff and parity validator -> variant-specific solver -> strategy/value checker -> benchmark integration. Store the exact variant and formal coverage with every result.
Existing alternatives and differentiation
PRISM-games already provides stochastic-game verification and strategy synthesis. A new backend should demonstrate a concrete improvement on published or user-representative benchmark cases.
Monetization hypothesis
Hypothesis: specialist integration or support contracts, initially AUD 5,000-20,000 for a bounded solver pilot. An open-source plugin can build adoption; willingness to pay for support is a separate question.
Validation experiment
Compare solved states and strategies with brute-force small games and established tools. Test negative rewards, large binary values, chance probabilities and parity conditions separately.
Conditions to reject or defer
Defer if the construction cannot be implemented usefully or if differences in payoff semantics make benchmark comparisons invalid.
Next concrete action
Review each variant's main statement and build a coverage matrix before selecting a single implementation target.
Source evidence
Repository sources are pinned to revision fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. Selected scope notes and manuscript statements have been reviewed to the extent described above; these links do not represent successful kernel checks.
Family 104
Subject: Quasipolynomial algorithms for mean-payoff, stochastic and parity games.
- Turn-Based Stochastic Mean-Payoff Games in Deterministic Quasipolynomial Time
- Mean-payoff parity games in quasipolynomial time
- Deterministic quasipolynomial-time mean-payoff games
- Randomized quasipolynomial-time mean-payoff games
- Formal scope notes
Current alternative sources
Primary documentation reviewed on 8 October 2026. Product availability demonstrates alternatives, not demand or willingness to pay for this proposal.