Multi-Objective Statistical Model Checking using Lightweight Strategy Sampling (extended version)
For verification engineers, this work enables quantitative verification of multiple objectives simultaneously with statistical guarantees, addressing a practical need that was previously unmet.
This paper presents the first statistical model checking approach for multi-objective Pareto queries, using lightweight strategy sampling. It introduces an incremental scheme that almost surely converges to a statistically sound confidence band around the true Pareto front, and proposes three heuristic approaches for finite-time underapproximation under a fixed sampling budget.
Statistical model checking delivers quantitative verification results with statistical guarantees. It scales to model sizes and model types that are out of reach for exhaustive, analytical techniques. So far, it has been used to evaluate one property value at a time only. Many practical problems, however, require finding the Pareto front of optimal tradeoffs between multiple objectives. In this paper, we present the first statistical model checking approach for such multi-objective Pareto queries, based on lightweight strategy sampling. We introduce an incremental scheme that almost surely converges to a statistically sound confidence band around the true Pareto front in the long run. To obtain a close underapproximation of the true front in finite time, we propose three heuristic approaches that try to make the best of an a-priori fixed sampling budget. We implement our new techniques in the modes simulator of the Modest Toolset, and show their effectiveness on benchmarks from the literature.