Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1649041,
author = {Ashok, Pranav and Butkova, Yuliya and Hermanns, Holger and Křetínský, Jan},
address = {Cham},
booktitle = {Automated Technology for Verification and Analysis. ATVA 2018},
doi = {http://dx.doi.org/10.1007/978-3-030-01090-4_19},
keywords = {Continuous-Time Markov Decision Processes; reachability; Partial Exploration},
howpublished = {tištěná verze "print"},
language = {eng},
location = {Cham},
isbn = {978-3-030-01089-8},
pages = {317-334},
publisher = {Springer},
title = {Continuous-Time Markov Decisions Based on Partial Exploration},
year = {2018}
}
TY - JOUR
ID - 1649041
AU - Ashok, Pranav - Butkova, Yuliya - Hermanns, Holger - Křetínský, Jan
PY - 2018
TI - Continuous-Time Markov Decisions Based on Partial Exploration
PB - Springer
CY - Cham
SN - 9783030010898
KW - Continuous-Time Markov Decision Processes
KW - reachability
KW - Partial Exploration
N2 - 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.
ER -
ASHOK, Pranav, Yuliya BUTKOVA, Holger HERMANNS and Jan KŘETÍNSKÝ. Continuous-Time Markov Decisions Based on Partial Exploration. In \textit{Automated Technology for Verification and Analysis. ATVA 2018}. Cham: Springer, 2018, p.~317-334. ISBN~978-3-030-01089-8. Available from: https://dx.doi.org/10.1007/978-3-030-01090-4\_{}19.
|
