Verification of markov decision processes using learning algorithms

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Authors

  • Tomáš Brázdil
  • Krishnendu Chatterjee
  • Martin Chmelík
  • Vojtěech Forejt
  • Jan Křetínský
  • Marta Kwiatkowska
  • Mateusz Ujma

Colleges, School and Institutes

External organisations

  • CEITEC, Masaryk University
  • University of Oxford
  • Ist Radioastron
  • Masaryk University

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.

Details

Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis
Subtitle of host publication 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014, Proceedings
EditorsFranck Cassez, Jean-Francois Raskin
Publication statusPublished - 2014
Event12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014 - Sydney, Australia
Duration: 3 Nov 20147 Nov 2014

Publication series

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

Conference

Conference12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014
CountryAustralia
CitySydney
Period3/11/147/11/14