Continuous-Time Markov Decisions Based on Partial Exploration

Pranav Ashok, Yuliya Butkova, Holger Hermanns, Jan Křetínský

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

12 Scopus citations

Abstract

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.

Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis - 16th International Symposium, ATVA 2018, Proceedings
EditorsChao Wang, Shuvendu K. Lahiri
PublisherSpringer Verlag
Pages317-334
Number of pages18
ISBN (Print)9783030010898
DOIs
StatePublished - 2018
Event16th International Symposium on Automated Technology for Verification and Analysis, ATVA 2018 - Los Angeles, United States
Duration: 7 Oct 201810 Oct 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11138 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference16th International Symposium on Automated Technology for Verification and Analysis, ATVA 2018
Country/TerritoryUnited States
CityLos Angeles
Period7/10/1810/10/18

Fingerprint

Dive into the research topics of 'Continuous-Time Markov Decisions Based on Partial Exploration'. Together they form a unique fingerprint.

Cite this