[WimmerHHB11] Reachability analysis for incomplete networks of Markov decision processes Wimmer, R.; Hahn, E. M.; Hermanns, H. and Becker, B. In 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE), pages 151-160, IEEE, 2011.
Downloads: pdf, bibURL: http://dx.doi.org/10.1109/MEMCOD.2011.5970522 Abstract. Assume we have a network of discrete-time Markov decision processes (MDPs) which synchronize via common actions. We investigate how to compute probability measures in case the structure of some of the component MDPs (so-called blackbox MDPs) is not known. We then extend this computation to work on networks of MDPs that share integer data variables of finite domain. We use a protocol which spreads information within a network as a case study to show the feasibility and effectiveness of our approach.