I will survey a body of work developed over the past 15 years or so, on algorithms for, and the computational complexity of, analyzing and model checking some important families of countably infinite state Markov chains, Markov decision processes (MDPs), and stochastic games. 1 will also highlight some of the open questions remaining in this area, including some algorithmic questions regarding arithmetic circuits.
展开▼