---
res:
  bibo_abstract:
  - "Markov decision processes (MDPs) are a fundamental model of decision making which
    exhibit non-deterministic choice as well as probabilistic uncertainty. Traditionally,
    verification assumes exact knowledge of the probabilities that govern the behaviour
    of an MDP. However, this assumption often is unrealistic, e.g. when modelling
    cyber-physical systems or biological processes. There, we can employ statistical
    model checking (SMC) to obtain an estimate of the MDP’s value (e.g. the maximal
    probability of reaching a goal state) that is close to the true value with high
    confidence (probably approximately correct). Model-based SMC algorithms sample
    the MDP and build a model of it by estimating all transition probabilities, essentially
    for every transition answering the question: “What are the odds?” However, so
    far the statistical methods employed by state-of-the-art SMC verification algorithms
    are quite naive or even compromise the correctness guarantees.\r\n\r\nOur first
    contribution is to survey, categorize, and analyse statistical methods, identifying
    those few that are most efficient and that provide suitable guarantees for the
    verification setting. Secondly, we propose improvements that exploit structural
    knowledge of the MDP. Both contributions generalize to many types of problem statements
    as they are largely independent of the setting. Moreover, our experimental evaluation
    shows that they lead to significant gains, reducing the number of samples that
    an SMC algorithm has to collect by up to two orders of magnitude.@eng"
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Tobias
      foaf_name: Meggendorfer, Tobias
      foaf_surname: Meggendorfer
      foaf_workInfoHomepage: http://www.librecat.org/personId=b21b0c15-30a2-11eb-80dc-f13ca25802e1
    orcid: 0000-0002-1712-2165
  - foaf_Person:
      foaf_givenName: Maximilian
      foaf_name: Weininger, Maximilian
      foaf_surname: Weininger
      foaf_workInfoHomepage: http://www.librecat.org/personId=02ab0197-cc70-11ed-ab61-918e71f56881
    orcid: 0000-0002-0163-2152
  - foaf_Person:
      foaf_givenName: Patrick
      foaf_name: Wienhöft, Patrick
      foaf_surname: Wienhöft
  bibo_doi: 10.1007/978-3-032-05792-1_11
  bibo_volume: 16143
  dct_date: 2025^xs_gYear
  dct_isPartOf:
  - http://id.crossref.org/issn/0302-9743
  - http://id.crossref.org/issn/1611-3349
  - http://id.crossref.org/issn/9783032057914
  dct_language: eng
  dct_publisher: Springer Nature@
  dct_title: What are the odds? Improving statistical model checking of Markov decision
    processes@
...
