The paper “Quantitative Model Checking of Discrete-Time Markov Processes” by Ilya Tkachev, Alexandru Mereacre, Joost-Pieter Katoen, and Alessandro Abate has been accepted for publication in Information and Computation.  The almost 50-page paper focuses on optimizing (repeated) reachability probabilities of events of interest defined
over general controlled discrete-time Markov processes.  Unlike known results
over finite-state models, this work considers general models evolving over uncountable spaces.