PyDSMC: Statistical Model Checking for Neural Agents Using the Gymnasium Interface

Timo P. Gros; Arnd Hartmanns; Ivo Hoese; Joshua Meyer; Nicola J. Müller; Verena Wolf

doi:10.1007/978-3-032-05792-1_8

PyDSMC: Statistical Model Checking for Neural Agents Using the Gymnasium Interface

Timo P. Gros^*
, Arnd Hartmanns
, Ivo Hoese
, Joshua Meyer
, Nicola J. Müller
, Verena Wolf

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

2 Downloads (Pure)

Abstract

Artificial intelligence (AI) has achieved remarkable success in sequential decision-making. However, evaluating its neural agents remains challenging, as current methods often rely on interpreting training curves only, overlooking key statistical factors. Existing tools that allow a formal evaluation also require white-box formal models, making them impractical for most AI benchmarks based on the black-box Gymnasium interface. We introduce PyDSMC, a lightweight and easy-to-use Python tool for statistical model checking of neural agents on arbitrary Gymnasium environments. PyDSMC automates the selection of statistical methods to compute confidence intervals, supporting both convergence-based and resource-limited evaluation settings. We empirically demonstrate the importance of rigorous agent evaluation and showcase PyDSMC ’s capabilities to more reliably judge and report an AI agent’s performance.

Original language	English
Title of host publication	Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems
Subtitle of host publication	Second International Joint Conference, QEST+FORMATS 2025, Proceedings
Editors	Pavithra Prabhakar, Andrea Vandin
Place of Publication	Cham
Publisher	Springer
Pages	134-156
Number of pages	23
Edition	1
ISBN (Electronic)	978-3-032-05792-1
ISBN (Print)	978-3-032-05791-4
DOIs	https://doi.org/10.1007/978-3-032-05792-1_8
Publication status	Published - 2026
Event	2nd International Joint Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems, QEST+FORMATS 2025 - Aarhus University, Aarhus, Denmark Duration: 26 Aug 2025 → 28 Aug 2025 Conference number: 2 https://www.qest.org/qest-formats-2025/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	16143 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	2nd International Joint Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems, QEST+FORMATS 2025
Abbreviated title	QEST+FORMATS 2025
Country/Territory	Denmark
City	Aarhus
Period	26/08/25 → 28/08/25
Other	QEST - International Conference on Quantitative Evaluation of SysTems; FORMATS - International Conference on Formal Modeling and Analysis of Timed Systems.
Internet address	https://www.qest.org/qest-formats-2025/

Keywords

This work was part of the MISSION (Models in Space Systems: Integration, Operation, and Networking) project, funded by the European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie Actions grant number 101008233.
2026 OA procedure

Access to Document

10.1007/978-3-032-05792-1_8

Conference paperFinal published version, 3.46 MBLicence: Taverne

Cite this

Gros, T. P., Hartmanns, A., Hoese, I., Meyer, J., Müller, N. J., & Wolf, V. (2026). PyDSMC: Statistical Model Checking for Neural Agents Using the Gymnasium Interface. In P. Prabhakar, & A. Vandin (Eds.), Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems: Second International Joint Conference, QEST+FORMATS 2025, Proceedings (1 ed., pp. 134-156). (Lecture Notes in Computer Science; Vol. 16143 LNCS). Springer. https://doi.org/10.1007/978-3-032-05792-1_8

Gros, Timo P. ; Hartmanns, Arnd ; Hoese, Ivo et al. / PyDSMC : Statistical Model Checking for Neural Agents Using the Gymnasium Interface. Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems: Second International Joint Conference, QEST+FORMATS 2025, Proceedings. editor / Pavithra Prabhakar ; Andrea Vandin. 1. ed. Cham : Springer, 2026. pp. 134-156 (Lecture Notes in Computer Science).

@inproceedings{bc8c68aa61614c848066daea8e945c7a,

title = "PyDSMC: Statistical Model Checking for Neural Agents Using the Gymnasium Interface",

abstract = "Artificial intelligence (AI) has achieved remarkable success in sequential decision-making. However, evaluating its neural agents remains challenging, as current methods often rely on interpreting training curves only, overlooking key statistical factors. Existing tools that allow a formal evaluation also require white-box formal models, making them impractical for most AI benchmarks based on the black-box Gymnasium interface. We introduce PyDSMC, a lightweight and easy-to-use Python tool for statistical model checking of neural agents on arbitrary Gymnasium environments. PyDSMC automates the selection of statistical methods to compute confidence intervals, supporting both convergence-based and resource-limited evaluation settings. We empirically demonstrate the importance of rigorous agent evaluation and showcase PyDSMC {\textquoteright}s capabilities to more reliably judge and report an AI agent{\textquoteright}s performance.",

keywords = "This work was part of the MISSION (Models in Space Systems: Integration, Operation, and Networking) project, funded by the European Union{\textquoteright}s Horizon 2020 research and innovation programme under Marie Sk{\l}odowska-Curie Actions grant number 101008233., 2026 OA procedure",

author = "Gros, \{Timo P.\} and Arnd Hartmanns and Ivo Hoese and Joshua Meyer and M{\"u}ller, \{Nicola J.\} and Verena Wolf",

note = "Publisher Copyright: {\textcopyright} The Author(s), under exclusive license to Springer Nature Switzerland AG 2026.; 2nd International Joint Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems, QEST+FORMATS 2025, QEST+FORMATS 2025 ; Conference date: 26-08-2025 Through 28-08-2025",

year = "2026",

doi = "10.1007/978-3-032-05792-1\_8",

language = "English",

isbn = "978-3-032-05791-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "134--156",

editor = "Pavithra Prabhakar and Andrea Vandin",

booktitle = "Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems",

address = "Germany",

edition = "1",

url = "https://www.qest.org/qest-formats-2025/",

}

Gros, TP, Hartmanns, A, Hoese, I, Meyer, J, Müller, NJ & Wolf, V 2026, PyDSMC: Statistical Model Checking for Neural Agents Using the Gymnasium Interface. in P Prabhakar & A Vandin (eds), Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems: Second International Joint Conference, QEST+FORMATS 2025, Proceedings. 1 edn, Lecture Notes in Computer Science, vol. 16143 LNCS, Springer, Cham, pp. 134-156, 2nd International Joint Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems, QEST+FORMATS 2025, Aarhus, Denmark, 26/08/25. https://doi.org/10.1007/978-3-032-05792-1_8

PyDSMC: Statistical Model Checking for Neural Agents Using the Gymnasium Interface. / Gros, Timo P.; Hartmanns, Arnd; Hoese, Ivo et al.
Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems: Second International Joint Conference, QEST+FORMATS 2025, Proceedings. ed. / Pavithra Prabhakar; Andrea Vandin. 1. ed. Cham: Springer, 2026. p. 134-156 (Lecture Notes in Computer Science; Vol. 16143 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - PyDSMC

T2 - 2nd International Joint Conference on Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems, QEST+FORMATS 2025

AU - Gros, Timo P.

AU - Hartmanns, Arnd

AU - Hoese, Ivo

AU - Meyer, Joshua

AU - Müller, Nicola J.

AU - Wolf, Verena

N1 - Conference code: 2

PY - 2026

Y1 - 2026

N2 - Artificial intelligence (AI) has achieved remarkable success in sequential decision-making. However, evaluating its neural agents remains challenging, as current methods often rely on interpreting training curves only, overlooking key statistical factors. Existing tools that allow a formal evaluation also require white-box formal models, making them impractical for most AI benchmarks based on the black-box Gymnasium interface. We introduce PyDSMC, a lightweight and easy-to-use Python tool for statistical model checking of neural agents on arbitrary Gymnasium environments. PyDSMC automates the selection of statistical methods to compute confidence intervals, supporting both convergence-based and resource-limited evaluation settings. We empirically demonstrate the importance of rigorous agent evaluation and showcase PyDSMC ’s capabilities to more reliably judge and report an AI agent’s performance.

AB - Artificial intelligence (AI) has achieved remarkable success in sequential decision-making. However, evaluating its neural agents remains challenging, as current methods often rely on interpreting training curves only, overlooking key statistical factors. Existing tools that allow a formal evaluation also require white-box formal models, making them impractical for most AI benchmarks based on the black-box Gymnasium interface. We introduce PyDSMC, a lightweight and easy-to-use Python tool for statistical model checking of neural agents on arbitrary Gymnasium environments. PyDSMC automates the selection of statistical methods to compute confidence intervals, supporting both convergence-based and resource-limited evaluation settings. We empirically demonstrate the importance of rigorous agent evaluation and showcase PyDSMC ’s capabilities to more reliably judge and report an AI agent’s performance.

KW - This work was part of the MISSION (Models in Space Systems: Integration, Operation, and Networking) project, funded by the European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie Actions grant number 101008233.

KW - 2026 OA procedure

UR - https://www.scopus.com/pages/publications/105020180483

U2 - 10.1007/978-3-032-05792-1_8

DO - 10.1007/978-3-032-05792-1_8

M3 - Conference contribution

AN - SCOPUS:105020180483

SN - 978-3-032-05791-4

T3 - Lecture Notes in Computer Science

SP - 134

EP - 156

BT - Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems

A2 - Prabhakar, Pavithra

A2 - Vandin, Andrea

PB - Springer

CY - Cham

Y2 - 26 August 2025 through 28 August 2025

ER -

Gros TP, Hartmanns A, Hoese I, Meyer J, Müller NJ, Wolf V. PyDSMC: Statistical Model Checking for Neural Agents Using the Gymnasium Interface. In Prabhakar P, Vandin A, editors, Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems: Second International Joint Conference, QEST+FORMATS 2025, Proceedings. 1 ed. Cham: Springer. 2026. p. 134-156. (Lecture Notes in Computer Science). Epub 2025 Oct 2. doi: 10.1007/978-3-032-05792-1_8