ISoLA 2024

International Symposium On Leveraging Applications of Formal Methods, Verification and Validation • Crete, Greece

Talk

Adaptive Stopping Algorithms Based on Concentration Inequalities

Time: Sunday, 3.11

Room: Room 1

Authors:

Abstract: Sampling is a key step of stochastic methods. In some contexts, minimizing the sample size can be of critical importance and determine by itself the viability of various approaches. Rethinking the way samples are generated can even lead to new algorithms, better suited than their alternatives to tackle specific real-world problems for which the sampling task is a costly step of the estimation process. For instance, strategies of formal verification and statistical model checking can be greatly improved by the use of adaptive stopping algorithms. Instead of initially computing the necessary sample size, those algorithms generate the samples progressively while continuously monitoring their progress along the way, allowing them to stop the sampling process as soon as possible. We present a generalization of two existing adaptive stopping algorithms for statistical model checking, and we show how this generalization can be exploited to derive tailor-made variations for specific use cases.

Paper: Download