---
res:
  bibo_abstract:
  - Statistical model checking estimates probabilities and expectations of interest
    in probabilistic system models by using random simulations. Its results come with
    statistical guarantees. However, many tools use unsound statistical methods that
    produce incorrect results more often than they claim. In this paper, we provide
    a comprehensive overview of tools and their correctness, as well as of sound methods
    available for estimating probabilities from the literature. For expected rewards,
    we investigate how to bound the path reward distribution to apply sound statistical
    methods for bounded distributions, of which we recommend the Dvoretzky-Kiefer-Wolfowitz
    inequality that has not been used in SMC so far. We prove that even reachability
    rewards can be bounded in theory, and formalise the concept of limit-PAC procedures
    for a practical solution. The modes SMC tool implements our methods and recommendations,
    which we use to experimentally confirm our results.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Carlos E.
      foaf_name: Budde, Carlos E.
      foaf_surname: Budde
  - foaf_Person:
      foaf_givenName: Arnd
      foaf_name: Hartmanns, Arnd
      foaf_surname: Hartmanns
  - 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
  - foaf_Person:
      foaf_givenName: Patrick
      foaf_name: Wienhöft, Patrick
      foaf_surname: Wienhöft
  bibo_doi: 10.1007/978-3-031-90643-5_9
  bibo_volume: 15696
  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/9783031906428
  dct_language: eng
  dct_publisher: Springer Nature@
  dct_title: Sound statistical model checking for probabilities and expected rewards@
...