The Hitchiker’s Guide to Stochastic Games

Markov Chain Gang - Spurious Fixpoints Suck

(Verse 1)
Yo, gather 'round, let me tell you 'bout what we found,
We're doing value iteration in a way that's sound
In stochastic games on graphs they're played round by round
There we complement VI with converging bounds

Arbitrary imprecision, yea, that ain't no more
We unify all the papers that came before
They were all restricted to particular objectives
Or to a single player, but we're not that selective

So you ask: Why should I care?
Does this solve any problems that I share?
Let me give you some words that are key:
Probabilistic model checking; game theory

If you wanna model check your stochastic game
But it's too large – scalability's the name of the aim
value iteration scales so well it's insane
and we fixed it – that's our claim to fame

(Hook 2x)
Bellman updates - can get stuck 
Spurious fixpoints - man they suck 
Can you stop? - I don't know
Why? - cause my bounds they are not close

(Verse 2)
Like I said, Bellmann updates they can linger
At a fixpoint that is wrong, for example bigger
Than it should, yea that's sour, baby, just like vinegar
Here's how to solve objectives that are fixpoint-linear

Step one: strategy recommender is what you need 
We prove that classical VI allows us to proceed
Step two: use the recommender to find SECs
Simple end components - get your mind outta the gutter!

Step three – now we really start flexin: 
observe that in a cycle you can only stay there or exit
So when you set your estimate to match the best of the two
You can force yourself to get out of the Bellman stuck blues

Our approach is objective-independent
it's novel, unifying, almost transcendant
We call our procedures deflate or inflate
And their based on asking: should I go or should I stay 

(Bridge)
This comes from IST in Klosterneuburg
But for real science I got that international support
I got my bro in Lancester, the Leipzig resort
And from Masaryk in Brno came the initial thought

All of us met at the TU of Munich
And our first draft of this was just cryptic and runic
With time we found the unifying solutions
VI's stopping - criteria - are our - contribution

(Hook 2x)
Bellman updates - can get stuck
Spurious fixpoints - man they suck
Can you stop? - Hey I know
Why? - cause I asked should I stay or go

(Verse 3)
So next time you're in doubt and you wonder what to do
With your stochastic system exhibiting a player or two
Remember always that guaranteed precision is crucial
And use our unified value iteration as the solution

Get the gist: check out our paper I'm praying
And if you ask: should I be going or staying
I tell you: stay, don't you hear the music is playing
Listen one more time to that sick hook cause it's slaying

(Hook 2x)
Bellman updates - can get stuck
Spurious fixpoints - man they suck
Can you stop? - Hey I know
Why? - cause I asked should I stay or go

Should I stay or should I go now?
Epsilon-close
Stop