---
res:
  bibo_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.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Tomáš
      foaf_name: Brázdil, Tomáš
      foaf_surname: Brázdil
  - foaf_Person:
      foaf_givenName: Krishnendu
      foaf_name: Chatterjee, Krishnendu
      foaf_surname: Chatterjee
      foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-4561-241X
  - foaf_Person:
      foaf_givenName: Martin
      foaf_name: Chmelik, Martin
      foaf_surname: Chmelik
      foaf_workInfoHomepage: http://www.librecat.org/personId=3624234E-F248-11E8-B48F-1D18A9856A87
  - foaf_Person:
      foaf_givenName: Vojtěch
      foaf_name: Forejt, Vojtěch
      foaf_surname: Forejt
  - foaf_Person:
      foaf_givenName: Jan
      foaf_name: Kretinsky, Jan
      foaf_surname: Kretinsky
      foaf_workInfoHomepage: http://www.librecat.org/personId=44CEF464-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-8122-2881
  - foaf_Person:
      foaf_givenName: Marta
      foaf_name: Kwiatkowska, Marta
      foaf_surname: Kwiatkowska
  - foaf_Person:
      foaf_givenName: David
      foaf_name: Parker, David
      foaf_surname: Parker
  - foaf_Person:
      foaf_givenName: Mateusz
      foaf_name: Ujma, Mateusz
      foaf_surname: Ujma
  bibo_doi: 10.1007/978-3-319-11936-6_8
  bibo_volume: 8837
  dct_date: 2014^xs_gYear
  dct_language: eng
  dct_publisher: Springer@
  dct_title: Verification of markov decision processes using learning algorithms@
...