×

Reward-bounded reachability probability for uncertain weighted MDPs. (English) Zbl 1475.68186

Jobstmann, Barbara (ed.) et al., Verification, model checking, and abstract interpretation. 17th international conference, VMCAI 2016, St. Petersburg, FL, USA, January 17–19, 2016. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 9583, 351-371 (2016).
Summary: In this paper we present a decision algorithm for computing maximal/minimal reward-bounded reachability probabilities in weighted MDPs with uncertainties. Even though an uncertain weighted MDP (UwMDP) represents an equivalent weighted MDP which may be exponentially larger, our algorithm does not cause an exponentially blow-up and will terminate in polynomial time with respect to the size of UwMDPs. We also define bisimulation relations for UwMDPs, which are compositional and can be decided in polynomial time as well. We develop a prototype tool and apply it to some case studies to show its effectiveness.
For the entire collection see [Zbl 1329.68030].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
PDFBibTeX XMLCite
Full Text: DOI