something something probabalisitc push down automata

A discrete timed markov chain is decisve from s wrt happy bro if probabilty of getting to happy bro + probability to reach sad guy is 1?

• finite Markov chains
• probabilisitic lossy channel systesm
• probablilistic vass
• noisy turing machines

Statistical Model checking

• number of good paths checked / number of paths checked