---
OA_place: publisher
OA_type: hybrid
_id: '19742'
abstract:
- lang: eng
  text: 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.
acknowledgement: This work was supported by the DFG through the Cluster of Excellence
  EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence Strategy)
  and the TRR 248 (see perspicuous-computing.science, project ID 389792660), by the
  European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie
  grant agreements 101008233 (MISSION), 101034413 (IST-BRIDGE), and 101067199 (ProSVED),
  by the EU under NextGenerationEU projects D53D23008400006 (Smartitude) under MUR
  PRIN 2022 and PE00000014 (SERICS) under MUR PNRR, by the Interreg North Sea project
  STORM_SAFE, and by NWO VIDI grant VI.Vidi.223.110 (TruSTy).
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Carlos E.
  full_name: Budde, Carlos E.
  last_name: Budde
- first_name: Arnd
  full_name: Hartmanns, Arnd
  last_name: Hartmanns
- first_name: Tobias
  full_name: Meggendorfer, Tobias
  id: b21b0c15-30a2-11eb-80dc-f13ca25802e1
  last_name: Meggendorfer
  orcid: 0000-0002-1712-2165
- first_name: Maximilian
  full_name: Weininger, Maximilian
  id: 02ab0197-cc70-11ed-ab61-918e71f56881
  last_name: Weininger
- first_name: Patrick
  full_name: Wienhöft, Patrick
  last_name: Wienhöft
citation:
  ama: 'Budde CE, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. Sound statistical
    model checking for probabilities and expected rewards. In: <i>31st International
    Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>.
    Vol 15696. Springer Nature; 2025:167-190. doi:<a href="https://doi.org/10.1007/978-3-031-90643-5_9">10.1007/978-3-031-90643-5_9</a>'
  apa: 'Budde, C. E., Hartmanns, A., Meggendorfer, T., Weininger, M., &#38; Wienhöft,
    P. (2025). Sound statistical model checking for probabilities and expected rewards.
    In <i>31st International Conference on Tools and Algorithms for the Construction
    and Analysis of Systems</i> (Vol. 15696, pp. 167–190). Hamilton, ON, Canada: Springer
    Nature. <a href="https://doi.org/10.1007/978-3-031-90643-5_9">https://doi.org/10.1007/978-3-031-90643-5_9</a>'
  chicago: Budde, Carlos E., Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger,
    and Patrick Wienhöft. “Sound Statistical Model Checking for Probabilities and
    Expected Rewards.” In <i>31st International Conference on Tools and Algorithms
    for the Construction and Analysis of Systems</i>, 15696:167–90. Springer Nature,
    2025. <a href="https://doi.org/10.1007/978-3-031-90643-5_9">https://doi.org/10.1007/978-3-031-90643-5_9</a>.
  ieee: C. E. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, and P. Wienhöft,
    “Sound statistical model checking for probabilities and expected rewards,” in
    <i>31st International Conference on Tools and Algorithms for the Construction
    and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15696, pp. 167–190.
  ista: 'Budde CE, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. 2025. Sound
    statistical model checking for probabilities and expected rewards. 31st International
    Conference on Tools and Algorithms for the Construction and Analysis of Systems.
    TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS,
    vol. 15696, 167–190.'
  mla: Budde, Carlos E., et al. “Sound Statistical Model Checking for Probabilities
    and Expected Rewards.” <i>31st International Conference on Tools and Algorithms
    for the Construction and Analysis of Systems</i>, vol. 15696, Springer Nature,
    2025, pp. 167–90, doi:<a href="https://doi.org/10.1007/978-3-031-90643-5_9">10.1007/978-3-031-90643-5_9</a>.
  short: C.E. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, P. Wienhöft, in:,
    31st International Conference on Tools and Algorithms for the Construction and
    Analysis of Systems, Springer Nature, 2025, pp. 167–190.
conference:
  end_date: 2025-05-08
  location: Hamilton, ON, Canada
  name: 'TACAS: Tools and Algorithms for the Construction and Analysis of Systems'
  start_date: 2025-05-03
date_created: 2025-05-25T22:17:08Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2025-06-02T09:45:41Z
day: '01'
ddc:
- '000'
department:
- _id: KrCh
doi: 10.1007/978-3-031-90643-5_9
ec_funded: 1
external_id:
  arxiv:
  - '2411.00559'
file:
- access_level: open_access
  checksum: d45856b503b1dd4f8f14c3566327225b
  content_type: application/pdf
  creator: dernst
  date_created: 2025-06-02T09:35:42Z
  date_updated: 2025-06-02T09:35:42Z
  file_id: '19770'
  file_name: 2025_TACAS_Budde.pdf
  file_size: 711271
  relation: main_file
  success: 1
file_date_updated: 2025-06-02T09:35:42Z
has_accepted_license: '1'
intvolume: '     15696'
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '05'
oa: 1
oa_version: Published Version
page: 167-190
project:
- _id: fc2ed2f7-9c52-11eb-aca3-c01059dda49c
  call_identifier: H2020
  grant_number: '101034413'
  name: 'IST-BRIDGE: International postdoctoral program'
publication: 31st International Conference on Tools and Algorithms for the Construction
  and Analysis of Systems
publication_identifier:
  eissn:
  - 1611-3349
  isbn:
  - '9783031906428'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
  record:
  - id: '19769'
    relation: research_data
    status: public
scopus_import: '1'
status: public
title: Sound statistical model checking for probabilities and expected rewards
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15696
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '19741'
abstract:
- lang: eng
  text: 'Quantitative automata model beyond-boolean aspects of systems: every execution
    is mapped to a real number by incorporating weighted transitions and value functions
    that generalize acceptance conditions of boolean w-automata. Despite the theoretical
    advances in systems analysis through quantitative automata, the first comprehensive
    software tool for quantitative automata (Quantitative Automata Kit, or QuAK) was
    developed only recently. QuAK implements algorithms for solving standard decision
    problems, e.g., emptiness and universality, as well as constructions for safety
    and liveness of quantitative automata. We present the architecture of QuAK, which
    reflects that all of these problems reduce to either checking inclusion between
    two quantitative automata or computing the highest value achievable by an automaton—its
    so-called top value. We improve QuAK by extending these two algorithms with an
    option to return, alongside their results, an ultimately periodic word witnessing
    the algorithm’s output, as well as implementing a new safety-liveness decomposition
    algorithm that can handle nondeterministic automata, making QuAK more informative
    and capable.'
acknowledgement: This work was supported in part by the ERC-2020-AdG 101020093.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Marek
  full_name: Chalupa, Marek
  id: 87e34708-d6c6-11ec-9f5b-9391e7be2463
  last_name: Chalupa
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000-0002-2985-7724
- first_name: Nicolas Adrien
  full_name: Mazzocchi, Nicolas Adrien
  id: b26baa86-3308-11ec-87b0-8990f34baa85
  last_name: Mazzocchi
- first_name: Naci E
  full_name: Sarac, Naci E
  id: 8C6B42F8-C8E6-11E9-A03A-F2DCE5697425
  last_name: Sarac
citation:
  ama: 'Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. Automating the analysis of
    quantitative automata with QuAK. In: <i>31st International Conference on Tools
    and Algorithms for the Construction and Analysis of Systems</i>. Vol 15696. Springer
    Nature; 2025:303-312. doi:<a href="https://doi.org/10.1007/978-3-031-90643-5_16">10.1007/978-3-031-90643-5_16</a>'
  apa: Chalupa, M., Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2025).
    Automating the analysis of quantitative automata with QuAK. In <i>31st International
    Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>
    (Vol. 15696, pp. 303–312). Springer Nature. <a href="https://doi.org/10.1007/978-3-031-90643-5_16">https://doi.org/10.1007/978-3-031-90643-5_16</a>
  chicago: Chalupa, Marek, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci
    E Sarac. “Automating the Analysis of Quantitative Automata with QuAK.” In <i>31st
    International Conference on Tools and Algorithms for the Construction and Analysis
    of Systems</i>, 15696:303–12. Springer Nature, 2025. <a href="https://doi.org/10.1007/978-3-031-90643-5_16">https://doi.org/10.1007/978-3-031-90643-5_16</a>.
  ieee: M. Chalupa, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Automating
    the analysis of quantitative automata with QuAK,” in <i>31st International Conference
    on Tools and Algorithms for the Construction and Analysis of Systems</i>, 2025,
    vol. 15696, pp. 303–312.
  ista: Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. 2025. Automating the analysis
    of quantitative automata with QuAK. 31st International Conference on Tools and
    Algorithms for the Construction and Analysis of Systems. , LNCS, vol. 15696, 303–312.
  mla: Chalupa, Marek, et al. “Automating the Analysis of Quantitative Automata with
    QuAK.” <i>31st International Conference on Tools and Algorithms for the Construction
    and Analysis of Systems</i>, vol. 15696, Springer Nature, 2025, pp. 303–12, doi:<a
    href="https://doi.org/10.1007/978-3-031-90643-5_16">10.1007/978-3-031-90643-5_16</a>.
  short: M. Chalupa, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 31st International
    Conference on Tools and Algorithms for the Construction and Analysis of Systems,
    Springer Nature, 2025, pp. 303–312.
corr_author: '1'
date_created: 2025-05-25T22:17:07Z
date_published: 2025-05-01T00:00:00Z
date_updated: 2026-04-07T12:02:57Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-031-90643-5_16
ec_funded: 1
external_id:
  arxiv:
  - '2501.16088'
file:
- access_level: open_access
  checksum: a27fa245be8d83421e9127b48a09c8af
  content_type: application/pdf
  creator: dernst
  date_created: 2025-06-02T08:13:11Z
  date_updated: 2025-06-02T08:13:11Z
  file_id: '19768'
  file_name: 2025_TACAS_ChalupaMarek.pdf
  file_size: 420669
  relation: main_file
  success: 1
file_date_updated: 2025-06-02T08:13:11Z
has_accepted_license: '1'
intvolume: '     15696'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Published Version
page: 303-312
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: 31st International Conference on Tools and Algorithms for the Construction
  and Analysis of Systems
publication_identifier:
  eissn:
  - 1611-3349
  isbn:
  - '9783031906428'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
related_material:
  record:
  - id: '20147'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: Automating the analysis of quantitative automata with QuAK
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 15696
year: '2025'
...