Continuous-Time Markov Decisions Based on Partial Exploration

Investor logo

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

ASHOK Pranav BUTKOVA Yuliya HERMANNS Holger KŘETÍNSKÝ Jan

Year of publication 2018
Type Article in Proceedings
Conference Automated Technology for Verification and Analysis. ATVA 2018
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-030-01090-4_19
Keywords Continuous-Time Markov Decision Processes; reachability; Partial Exploration
Description We provide a framework for speeding up algorithms for time-bounded reachability analysis of continuous-time Markov decision processes. The principle is to find a small, but almost equivalent subsystem of the original system and only analyse the subsystem. Candidates for the subsystem are identified through simulations and iteratively enlarged until runs are represented in the subsystem with high enough probability. The framework is thus dual to that of abstraction refinement. We instantiate the framework in several ways with several traditional algorithms and experimentally confirm orders-of-magnitude speed ups in many cases.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.