Multi-Objective Statistical Model Checking using Lightweight Strategy Sampling (extended version)

TL;DR

This paper introduces a novel multi-objective statistical model checking method using lightweight strategy sampling, enabling the approximation of Pareto fronts in models with nondeterminism, which was previously unaddressed.

Contribution

It presents the first approach for multi-objective Pareto queries in statistical model checking, including an incremental convergence scheme and heuristic methods for finite-time approximation.

Findings

Effective convergence to true Pareto front bounds

Heuristic methods improve finite-time approximation

Implementation in Modest Toolset shows practical effectiveness

Abstract

Statistical model checking delivers quantitative verification results with statistical guarantees by applying Monte Carlo simulation to formal models. 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 possibly conflicting optimisation objectives. In this paper, we present the first statistical model checking approach for such multi-objective Pareto queries, using lightweight strategy sampling to optimise over the model's nondeterministic choices. We first introduce an incremental scheme that almost surely converges to a statistically sound confidence band bounding the true Pareto front from both sides in the long run. To obtain a close underapproximation of the true front in finite time, we then propose three heuristic approaches that try to make the best of an a-priori fixed sampling budget. We implement our new techniques in the Modest Toolset's 'modes' simulator, and experimentally show their effectiveness on quantitative verification benchmarks.