Verification of markov decision processes using learning algorithms Conference Paper


Author(s): Brázdil, Tomáš; Chatterjee, Krishnendu; Chmelík, Martin; Forejt, Vojtěch; Křetínský, Jan; Kwiatkowska, Marta Z; Parker, David; Ujma, Mateusz
Title: Verification of markov decision processes using learning algorithms
Title Series: LNCS
Affiliation IST Austria
Abstract: We present a general framework for applying machine-learning algorithms to the verification of Markov decision processes (MDPs). The primary goal of these techniques is to improve performance by avoiding an exhaustive exploration of the state space. Our framework focuses on probabilistic reachability, which is a core property for verification, and is illustrated through two distinct instantiations. The first assumes that full knowledge of the MDP is available, and performs a heuristic-driven partial exploration of the model, yielding precise lower and upper bounds on the required probability. The second tackles the case where we may only sample the MDP, and yields probabilistic guarantees, again in terms of both the lower and upper bounds, which provides efficient stopping criteria for the approximation. The latter is the first extension of statistical model checking for unbounded properties inMDPs. In contrast with other related techniques, our approach is not restricted to time-bounded (finite-horizon) or discounted properties, nor does it assume any particular properties of the MDP. We also show how our methods extend to LTL objectives. We present experimental results showing the performance of our framework on several examples.
Conference Title: ALENEX: Algorithm Engineering and Experiments
Volume: 8837
Conference Dates: November 3-7, 2014
Conference Location: Sydney, Australia
ISBN: 978-1-61197-319-8
Publisher: Society of Industrial and Applied Mathematics  
Date Published: 2014-11-01
Start Page: 98
End Page: 114
URL:
DOI: 10.1007/978-3-319-11936-6_8
Notes: This research was funded in part by the European Research Council (ERC) under grant agreement 267989 (QUAREM), 246967 (VERIWARE) and 279307 (Graph Games), by the EU FP7 project HIERATIC, by the Austrian Science Fund (FWF) projects S11402-N23 (RiSE), S11407-N23 (RiSE) and P23499-N23, by the Czech Science Foundation grant No P202/12/P612, by EPSRC project EP/K038575/1 and by the Microsoft faculty fellows award.
Open access: yes (repository)