Public Thesis Defense of Maxime PARMENTIER - ICTEAM
sst |
Improvements in Statistical Model Checking : Estimation, Optimization, Parallelization by Maxime PARMENTIER -
Tuesday, 26 August 2025 at 2:00 p.m. - Room BARB92 - Place Sainte-Barbe - 1348 Louvain-la-Neuve
Statistical model checking (SMC) offers a wide collection of frameworks and algorithms for the verification of complex programs or systems. SMC goes beyond testing and code analysis but circumvents the state-explosion problem that limits the usability of pure formal methods by only considering a subset of possible execution traces and relying on strong statistical results to provide quantifiable guarantees for the design requirements.
This thesis enhances the efficiency and expands the range of application of SMC in multiple ways. First, we develop a theory of stopping algorithms based on concentration inequalities. These estimation algorithms are shown to require significantly smaller sample sizes than the methods that are currently implemented in existing tools. These stopping algorithms can therefore replace basic Monte-Carlo based approaches in SMC strategies to greatly improve their scalability. Second, we present an improved version of the Smart Sampling algorithm, a SMC algorithm for the optimization of policies for Markov decision processes. Third, we show and analyze the huge impact parallelization can have on the applicability of SMC to deal with real-world problems. In particular, we discuss the requirements the parallelization architecture must hold to avoid the introduction of bias in the verification process. Fourth, we build a new SMC framework for temporal networks and show how the fundamental ideas of SMC can help solve difficult planning problems.
These improvements not only tackle some of the long-standing challenges of the field, such as the rare event problem or the never-ending issue of scalability, they also highlight the limitations of elementary methods for sample generation that only rely on non-guided randomness and allow us to provide suggestions and paths to explore to further improve SMC in the coming future.
Jury members
- Prof. Charles Pecheur (UCLouvain) (Supervisor)
- Prof. Peter Van Roy (UCLouvain) (Chairperson)
- Prof. Kim Mens (UCLouvain) (Secretary)
- Prof. Pierre-Yves Schobbens (UNamur)
- Prof. Maxime Cordy (University of Luxembourg)
- Prof. Arnd Hartmanns (University of Twente)