@inproceedings{19742,
  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.},
  author       = {Budde, Carlos E. and Hartmanns, Arnd and Meggendorfer, Tobias and Weininger, Maximilian and Wienhöft, Patrick},
  booktitle    = {31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  isbn         = {9783031906428},
  issn         = {1611-3349},
  location     = {Hamilton, ON, Canada},
  pages        = {167--190},
  publisher    = {Springer Nature},
  title        = {{Sound statistical model checking for probabilities and expected rewards}},
  doi          = {10.1007/978-3-031-90643-5_9},
  volume       = {15696},
  year         = {2025},
}

@inproceedings{19741,
  abstract     = {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.},
  author       = {Chalupa, Marek and Henzinger, Thomas A and Mazzocchi, Nicolas Adrien and Sarac, Naci E},
  booktitle    = {31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  isbn         = {9783031906428},
  issn         = {1611-3349},
  pages        = {303--312},
  publisher    = {Springer Nature},
  title        = {{Automating the analysis of quantitative automata with QuAK}},
  doi          = {10.1007/978-3-031-90643-5_16},
  volume       = {15696},
  year         = {2025},
}