Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Pedro R. D'Argenio, Arnd Hartmanns, Patrick Wienhöft, Mark van Wijk

TL;DR

The paper advances the verification of systems with multiple probabilistic objectives by extending statistical model checking to Pareto-front queries using lightweight strategy sampling. It introduces an incremental convergence scheme that yields simultaneous confidence bands for the true Pareto front and three fixed-budget heuristics (WVR, FIB, FSB) to obtain high-quality fronts within finite time, all in constant memory. Implemented in the Modes simulator of the Modest Toolset, the approach is demonstrated on 34 models, showing scalability beyond Storm’s multi-objective PMC on larger models and delivering nontrivial Pareto fronts for challenging instances. The work provides concrete methodological guarantees, practical guidance on algorithm choice, and broadens the applicability of SMC to multi-objective verification problems.

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.

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

TL;DR

The paper advances the verification of systems with multiple probabilistic objectives by extending statistical model checking to Pareto-front queries using lightweight strategy sampling. It introduces an incremental convergence scheme that yields simultaneous confidence bands for the true Pareto front and three fixed-budget heuristics (WVR, FIB, FSB) to obtain high-quality fronts within finite time, all in constant memory. Implemented in the Modes simulator of the Modest Toolset, the approach is demonstrated on 34 models, showing scalability beyond Storm’s multi-objective PMC on larger models and delivering nontrivial Pareto fronts for challenging instances. The work provides concrete methodological guarantees, practical guidance on algorithm choice, and broadens the applicability of SMC to multi-objective verification problems.

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.

Paper Structure

This paper contains 34 sections, 2 theorems, 1 equation, 12 figures, 3 tables, 5 algorithms.

Table of Contents

  1. Introduction
  2. Related work.
  3. Background
  4. Markov decision processes
  5. Single-objective properties.
  6. Multi-objective properties.
  7. Statistical model checking.
  8. Lightweight strategy sampling.
  9. Multi-Objective SMC
  10. Approximating the Pareto front.
  11. Multiple comparisons.
  12. Incremental Sampling with Convergence
  13. Strategy Selection Heuristics
  14. Fixed-Budget Sampling
  15. Weight vector refinement.
  16. ...and 19 more sections

Key Result

lemma 1

$\underline{C}$ is an underapproximation with probability $\gamma$.

Figures (12)

  • Figure 1: An example MDP and the corresponding expected-reward Pareto fronts
  • Figure 2: Sampled strategies per sampled runs in \ref{['alg:incremental']} for $d = 2, \varepsilon = 0.01, \alpha = 0.1$
  • Figure 3: Statistical comparison of sampled strategies.
  • Figure 4: Criteria for discarding unpromising strategies.
  • Figure 5: Number of strategies in each iteration using the simple heuristic
  • ...and 7 more figures

Theorems & Definitions (8)

  • definition 1
  • lemma 1
  • proof : sketch
  • remark 1
  • lemma 2
  • proof : sketch
  • definition 2: A simple rule
  • definition 3