1 Introduction↩︎

Statistical model checking (SMC) [1]–[3] is a popular alternative to probabilistic model checking (PMC) [4], [5] for applications where the latter runs into the state space explosion problem due to its exhaustive nature, or where no effective PMC algorithm is available for the model class at hand. SMC circumvents these limitations by applying Monte Carlo simulation: Given an effectively executable probabilistic model \(M\) and property of interest \(\phi\), it performs random executions (or simulation runs) of \(M\) to obtain samples for the satisfaction or numeric value of \(\phi\). Given a desired confidence level, SMC then computes a confidence interval around the satisfaction probability or expected value of \(\phi\), providing a statistical correctness guarantee. The core types of properties handled by PMC and SMC are reachability probabilities and expected accumulated rewards [6], [7], and both can be extended to compute probabilities for \(\omega\)-regular objectives in e.g. LTL [8] [9], [10]. PMC and more recently SMC [11] have also been extended to other quantities like quantiles [12], [13] and conditional value at risk [14]. In practice, we often face tradeoffs between multiple properties, such as maximising a satellite’s expected utility without depleting its battery [15], or balancing cost and comfort in heat-pump control [16]. That is, for a probabilistic model with controllable nondeterministic choices, we want to choose among the set of Pareto-optimal control strategies: those where no change can be made that improves the value for at least one property without worsening any other. While PMC algorithms for such multi-objective problems are more than a decade old [17], [18] and cover various models [19] and properties [20], we are not aware of any work that brings the advantages of SMC to the multi-objective setting.

In this paper, we present the first multi-objective SMC approach for Pareto queries. Its memory usage is constant in the size of the model’s state space, preserving the distinguishing advantage of SMC. It uses lightweight strategy sampling (LSS) [21] to evaluate many randomly chosen control strategies w.r.t. all objectives at hand, and from the resulting data constructs a statistically sound approximation of the (unknown) true Pareto front.

We first propose an incremental scheme that keeps sampling batches of new strategies, continuously refining an under- and overapproximation of the Pareto front. Assuming ideal LSS and taking care to properly handle statistical error accumulation, the two approximations almost surely converge to a simultaneous confidence band for the true Pareto front in the long run. Second, we introduce three fixed-budget algorithms aiming to find the best approximation of the Pareto front in finite time. They deliver statistically sound simultaneous lower bounds, since obtaining guarantees on upper bounds is impossible in finite time.

We implement our approach in the Modest Toolset [22]’s modes simulator [23] to experimentally evaluate the effectiveness of SMC-based multi-objective model checking and compare the three fixed-budget algorithms, using benchmarks from the quantitative verification and reinforcement learning (RL) [24] literature. Our SMC approaches deliver nontrivial fronts for instances too large (in terms of state space size and dimensionality of the multi-objective query) to be checked by Storm’s [25] multi-objective PMC engine. We compare the quality of our approximation with the Pareto fronts computed by Storm where possible. We use Markov decision process (MDP) [26]–[28] models in this paper, but our work directly extends to any model class supported by LSS, e.g. Markov automata [29], [30] and probabilistic timed automata [31]–[33].

1.0.0.1 Related work.

Multi-objective PMC uses linear programming [17], [34] or value iteration [18], [19]. It is implemented in Storm, Prism [35], and ePMC [36]; see [37] for a summary of the state of the art. While PMC can provide hard (non-statistical) guarantees, it requires exploration of the model’s state space. SMC, in contrast, samples instead of exploring, avoiding the state space explosion problem and easily handling models with billions of states [38].

Uppaal Smc [39] can compare the values of two properties via SMC on a fully stochastic model. Uppaal Stratego [40] brings together SMC and nondeterminism: It first finds a most permissive strategy for a set of hard constraints via real-time model checking [41], then among the choices allowed by this strategy, uses RL to optimise a “soft” quantity [42], which is finally evaluated via SMC. Stratego thus solves a lexicographic objectives problem [43], [44] and performs one-dimensional quantitative optimisation only. We, in contrast, determine the trade-offs between multiple equal-priority probabilistic properties. We do so in constant memory, while both Stratego’s initial model checking and RL store per-state information, potentially limiting scalability. The latter equally applies to other RL-based multi-objective analysis approaches [45], [46].

The general field of multi-objective optimisation [47], [48] uses many different techniques such as evolutionary algorithms [49]–[51], particle swarm optimisation [52], or ant colony optimisation [53]. These are typically applied to functions of real numbers but can be extended to MDPs [54], [55]. Like our methods, in finite time, these approaches provide lower bounds only. They however require more than constant memory and typically do not offer statistical guarantees.

2 Background↩︎

A reward structure provides a reward when moving from one state to another. We call \(\delta(s, a)\) for \(a \in \mathcal{A}(s)\) a transition; its branches are \(\{\, s' \mid \delta(s, a)(s') > 0 \,\}\).

A path is a sequence \(s_0\, a_0\, \ldots \in (\mathcal{S} \times \mathcal{A})^\omega\) s.t.\(\forall i\colon a_i \in \mathcal{A}(s_i) \wedge \delta(s, a)(s_{i+1}) > 0\). In an MDP, the choice of action in each state is nondeterministic. A probabilistic memoryless strategy \(\sigma \colon \mathcal{S} \rightarrow (\mathcal{A} \to [0,1])\) with \(\sum_{a \in \mathcal{A}(s)}\sigma(s)(a) = 1\) makes this choice in all states \(s\). If \(\forall s\,\exists\,a\colon \sigma(s)(a) = 1\), the strategy is deterministic memoryless (DM). When removing all state-actions not chosen by \(\sigma\), we get the induced discrete-time Markov chain \(M|_\sigma\), on which we can construct probability measures \(\mathbb{P}_\sigma^{M,s}\) on the measurable sets of paths starting in \(s\) [56].

2.0.0.1 Single-objective properties.

The optimal reachability probabilities of a set of goal states \(G \subset \mathcal{S}\) are \(\mathrm{P}_\mathrm{\!min}(\diamond\, G) \mathrel{\vbox{\offinterlineskip\ialign{\hfil##\hfil\cr{\tiny \rm def}\cr\noalign{\kern 0.30ex}=\cr}}}\textstyle\inf_{\sigma} \mathrm{P}^\sigma(\diamond\, G)\) and \(\mathrm{P}_\mathrm{\!max}(\diamond\, G) \mathrel{\vbox{\offinterlineskip\ialign{\hfil##\hfil\cr{\tiny \rm def}\cr\noalign{\kern 0.30ex}=\cr}}}\textstyle\sup_{\sigma} \mathrm{P}^\sigma(\diamond\, G)\) where \(\mathrm{P}^\sigma(\diamond\, G) \mathrel{\vbox{\offinterlineskip\ialign{\hfil##\hfil\cr{\tiny \rm def}\cr\noalign{\kern 0.30ex}=\cr}}}\mathbb{P}_\sigma^{M,s_\mathit{init}}(\Pi_G)\) with \(\Pi_G\) the set of paths that contain a state in \(G\). The optimal expected rewards to reach a goal are \(\mathrm{E}_\mathrm{min}^\mathcal{R}(\diamond\, G) \mathrel{\vbox{\offinterlineskip\ialign{\hfil##\hfil\cr{\tiny \rm def}\cr\noalign{\kern 0.30ex}=\cr}}}\textstyle\inf_{\sigma} \mathrm{E}^{\mathcal{R},\sigma}(\diamond\, G)\) and \(\mathrm{E}_\mathrm{max}^\mathcal{R}(\diamond\, G) \mathrel{\vbox{\offinterlineskip\ialign{\hfil##\hfil\cr{\tiny \rm def}\cr\noalign{\kern 0.30ex}=\cr}}}\textstyle\sup_{\sigma} \mathrm{E}^{\mathcal{R},\sigma}(\diamond\, G)\) where \(\mathrm{E}^{\mathcal{R},\sigma}(\diamond\, G) \mathrel{\vbox{\offinterlineskip\ialign{\hfil##\hfil\cr{\tiny \rm def}\cr\noalign{\kern 0.30ex}=\cr}}}\mathbb{E}_\sigma^{M,s_\mathit{init}}(R^\mathcal{R}_G)\), \(\mathbb{E}_\sigma^{M,s_\mathit{init}}(r)\) is the expectation of random variable \(r\) under \(\mathbb{P}_\sigma^{M,s_\mathit{init}}\), and \(R^\mathcal{R}_G\) maps each path to the sum of the rewards incurred up to the first state in \(G\), or to \(\infty\) if the path does not contain such a state. Note that we consider undiscounted reachability rewards, not total-reward or discounted properties. We restrict to contracting MDPs, i.e. MDPs that do not contain nontrivial end components. This is common in the literature [57], [58], suffices for simulation runs to almost surely terminate—otherwise, we would need more powerful checks that require more than constant memory [10]—and avoids semantic issues which cause current multi-objective PMC tools to return inconsistent results on non-contracting MDPs [59]. In this setting, for the properties we consider, DM strategies are optimal, even if the model has both positive and negative rewards [58]. For a property \(\phi = \mathrm{P}_\mathit{\!opt}(\diamond\, G)\) or \(\phi = \mathrm{E}_\mathit{opt}^\mathcal{R}(\diamond\, G)\), we write \(\phi(\sigma)\) for \(\mathrm{P}^\sigma(\diamond\, G)\) or \(\mathrm{E}^{\mathcal{R},\sigma}(\diamond\, G)\), respectively.

2.0.0.2 Multi-objective properties.

Given \(\phi_1, \ldots, \phi_d\), the multi-objective property \(\phi = \mathrm{multi}(\phi_1, \ldots, \phi_d)\) asks for the Pareto front over all the properties. The achievable set \(\mathit{Ach}(\phi)\) contains all points \(\langle v_1, \ldots, v_d \rangle \in \mathbb{R}^d\) for which \(\exists\,\sigma\colon \phi_1(\sigma) \sim_1 v_1 \wedge \ldots \wedge \phi_d(\sigma) \sim_d v_d\) where \({\sim_i} = {\leq}\) if \(\phi_i\) is a \({\cdot}_\mathrm{max}\) property and \({\sim_i} = {\geq}\) else. A point \(v = \langle v_1, \ldots, v_d \rangle \in \mathit{Ach}(\phi)\) is Pareto-optimal if no other point \(\langle v_1', \ldots, v_d' \rangle\neq v\) with \(\forall i\colon v_i \sim_i v_i'\) is achievable; these points form the Pareto front.

MDP with multi-objective combinations of reachability probabilities and expected rewards can be transformed into MDP with combinations of only total rewards [18], for which memoryless strategies are Pareto-optimal [19]. The Pareto front is the convex hull of a finite set of corner points resulting from DM strategies; all its other points are convex combinations of the corners resulting from probabilistic strategies. Note that, for contracting MDPs, [19] also removes [18]’s restriction to non-negative rewards. An underapproximation of the achievable set (and thus the Pareto front) is a convex set of achievable but not necessarily Pareto-optimal points; an overapproximation, conversely, is a concave set of unachievable or Pareto-optimal points.

2.0.0.3 Statistical model checking.

Given a fully stochastic executable formal model (e.g. a large Markov chain compactly specified in a high-level modelling language), a property \(\phi\) that can be evaluated to a real value on a finite path, and user-specified number of runs \(n\) and confidence level \(\gamma \in (0, 1)\), we can perform statistical model checking (SMC): Randomly—using a pseudo-random number generator (PRNG) to implement the model’s probabilistic choices—perform \(n\) simulation runs, i.e. generate \(n\) random paths, evaluate \(\phi\) on each path to obtain samples \(X_1, \ldots, X_n\), compute the sample mean \(\hat{x} = \frac{1}{n}\sum_{i=1}^n X_i\) and a confidence interval (CI) \(I = [l, u] \ni \hat{x}\), and return the pair \(\langle \hat{x}, I \rangle\). Various methods exist to compute sound CIs [7] which guarantee that, when repeating the SMC procedure many times, in the limit \((100 \cdot \gamma)\,\%\) or more of the intervals contain the property’s (unknown) true value. The interval’s precision is \(\varepsilon = \frac{1}{2}(u - l)\); for many methods, we can precompute the \(n\) needed to achieve a given \(\varepsilon\).

2.0.0.4 Lightweight strategy sampling.

To apply SMC to nondeterministic models like MDPs, we need to simulate under a given strategy. Many SMC tools implicitly use the uniform random strategy. Lightweight strategy sampling (LSS) allows simulating many different strategies using a constant-memory representation for each, e.g. a 32-bit integer. When simulating with such a strategy identifier \(\sigma\) and encountering a state \(s\) with \(|\mathcal{A}(s)| = k > 1\), LSS chooses the \((\mathcal{H}(\sigma . s) \mathbin{\mathrm{mod}} k + 1)\)-th action (for some fixed ordering of \(\mathcal{A}(s)\)) where \(\mathcal{H}\) is a hash function and \(\sigma . s\) is the concatenation of the bitstring representations of \(\sigma\) and \(s\). In this way, LSS implements a DM strategy. By feeding different information into \(\mathcal{H}\), LSS can easily provide history-dependent or partially-informed [30], [60], [61] strategies as well. Good \(\mathcal{H}\) ensure that small changes in the input bits, in particular in \(\sigma\), have large effects on the output, to cover as much of the strategy space as uniformly as possible. Thus strategy identifiers are “opaque”, i.e. their values are not connected to their action choices in any systematic way.²

An MDP’s set of DM strategies—its strategy space—is vast but finite. We use 32-bit strategy identifiers, covering up to \(2^{32}\) strategies; while a large space to sample from, it will be smaller than the strategy space of many interesting MDPs. We consider this a practical limitation (that could be mitigated by moving to larger identifiers); in the theoretical arguments we make in the following sections, we assume ideal LSS where by uniformly sampling identifiers we will almost surely eventually encounter every DM strategy. We use a PRNG \(\mathfrak{P}\) to sample strategy identifiers; by initialising \(\mathfrak{P}\) with a fixed strategy seed, we can repeatedly sample the same sequence of strategies to make our experiments more repeatable.

3 Multi-Objective SMC↩︎

We present an incremental scheme and three fixed simulation budget algorithms. The latter use heuristics to discard seemingly suboptimal strategies. Fix an MDP as in 1, \(\phi = \mathrm{multi}(\phi_1, \ldots, \phi_d)\), and confidence level \(\gamma = 1 - \alpha\). Recall that the Pareto front’s corner points arise from DM strategies after the MDP transformation of [18], which essentially adds one Boolean state variable per property \(\phi_i\) to track whether its goal set has been reached.

3.0.0.1 Approximating the Pareto front.

All our approaches use LSS to sample deterministic strategies with \(d\) bits of memory, which track the visited goal sets to implement the transformation of [18] on-the-fly, and evaluate them via SMC. For each strategy \(\sigma\), we thus obtain \(d\) pairs \(\langle \hat{x}^\sigma_i, I^\sigma_i \rangle\) of a sample mean and a CI with precision \(\varepsilon_{i}^{\sigma}\) for each dimension, \(i \in \{\,1, \ldots, d\,\}\); together, the one-dimensional CIs describe a \(d\)-dimensional confidence box \(B_\sigma\) around the multi-objective sample mean \(\hat{x}^\sigma = \langle \hat{x}^\sigma_1, \ldots, \hat{x}^\sigma_d \rangle\). We ensure that the boxes for the evaluated strategies are all simultaneously correct with a-priori probability \(\gamma\) (requirement 1). We write \(\mathit{SMC}(\sigma, \gamma, \ldots)\) for the invocation of SMC with LSS for strategy identifier \(\sigma\) and statistical parameters \(\gamma, \ldots\) that returns \(\langle \hat{x}_\sigma, B_\sigma \rangle\) satisfying requirement 1. The convex hull of the “most pessimistic” corners of all boxes then bounds a candidate underapproximation \(\underline{C}\) of the Pareto front; using the “most optimistic” corners gives a candidate overapproximation \(\overline{C}\). Given a function \(\mathit{stat}\) mapping strategy identifiers to \(\langle \hat{x}^\sigma, B_\sigma \rangle\) pairs, we also write \(\underline{C}(\mathit{stat})\) and \(\overline{C}(\mathit{stat})\) to refer to the respective convex-hull computations.

3.0.0.2 Multiple comparisons.

We perform SMC (1) for each strategy (2) for each dimension, but want all confidence boxes to be correct simultaneously with probability \(\gamma\). If we build a CI for each strategy and dimension with confidence \(\gamma\), then at least one CI is wrong with probability \(\gg 1-\gamma\). There are two common ways to counteract this multiple comparisons problem: (1) In case of statistical independence, e.g. for the different strategies (since we perform separate simulation runs for each), Šidák correction [62] can be applied. That is, when sampling \(m\) strategies, request confidence \(\gamma_\sigma = \gamma^\frac{1}{m}\) for each strategy. (2) Within a call to \(\mathit{SMC}(\sigma, \gamma_\sigma, \ldots)\), all dimensions are estimated from the same simulation runs, so their CIs are not statistically independent. Then Bonferroni correction [63] resp.the union bound can be used, which requires \(\sum_{i=1}^k \alpha_i \leq \alpha\) for \(k\) CIs. Thus the error budget for each dimension can be set to e.g. \(\alpha_\sigma/d\) with \(\alpha_\sigma = 1 - \gamma_\sigma\). Šidák correction is harder to work with if we want to distribute the error budget unevenly, and only slightly more efficient than Bonferroni/the union bound beyond very small numbers of comparisons [64]. We thus use the latter throughout.

3.1 Incremental Sampling with Convergence↩︎

Our incremental scheme indefinitely samples batches of \(m\) strategies as shown in 3, updating \(\underline{C}\) and \(\overline{C}\) whenever a strategy has been evaluated. When interrupted, it returns the current candidate approximations \(\underline{C}\) and \(\overline{C}\). For 1 to hold at any interruption point, we need to divide the error budget \(\alpha\) over an a priori unknown number of batches. We use the union bound and a user-specified factor \(f \in (0,1)\): The \(i\)-th batch gets error budget \((1 - f)^{i-1} \cdot f \cdot \alpha\). Each batch’s budget is then divided equally among the \(m\) strategies. We parametrise the SMC invocations in line [alg:incremental:SMC] with precision \(\varepsilon\), not the number of runs \(n\); in this way, as \(\alpha\) decreases from batch to batch, the number of runs performed per strategy increases. If we fixed \(n\) instead, then \(\varepsilon\) would increase, resulting in larger and larger boxes for later strategies.

Thus, in the limit, we are \(\gamma\)-confident that the true Pareto front is fully enveloped by \(\underline{C}\) and \(\overline{C}\): they form a simultaneous \(\gamma\) confidence band for the true front.

2 holds independently of the values chosen for \(m\) and \(f\). The error budget assigned to a strategy determines the number of simulation runs needed in \(\mathit{SMC}(\sigma, \gamma', \varepsilon)\). A larger \(f\) results in a higher budget for earlier batches, requiring more runs in later batches to achieve the fixed precision \(\varepsilon\). A larger batch size \(m\) distributes each batch’s budget over more strategies, lowering the budget for earlier strategies. An example of these tradeoffs is visualised in [fig:approximation-settings:middle], using the Clopper-Pearson interval [65] and \(d = 2, \varepsilon = 0.01, \alpha = 0.1\). On the horizontal axis, the number of runs performed is a proxy for the runtime needed; completing the evaluation of more strategies (higher values on the vertical axis) with fewer runs is “better”. As expected, the combination of high \(f = 0.5\) and low \(m = 100\) starts fast but is overtaken by more conservative approaches in the long run. For large batch sizes, however, the influence of dividing \(\alpha\) is small in practice.

3.2 Fixed-Budget Sampling↩︎

In practice, we only have finite time. We propose three algorithms—weight vector refinement (WVR), fixed iteration budget (FIB), and fixed strategy budget (FSB)—that try to statistically approximate the achievable set as closely as possible in a fixed simulation budget. They use heuristics to select “promising” strategies, performing fewer simulation runs for seemingly suboptimal ones so that promising ones can be estimated more precisely or more strategies can be sampled. We describe our heuristics in 3.3; for now, assume one is given as a function \(\mathsf{select\_candidates}\colon 2^{\Sigma} \to 2^{\Sigma}\) that, given a candidate set of strategies, returns a subset of promising strategies. WVR adapts multi-objective PMC [18], [19] to the SMC setting, while FIB transfers smart sampling [66] from single-objective to multi-objective SMC. FSB adds dynamic addition of strategies to FIB. While many more schemes are imaginable, these are fundamental corner points.

Since only finitely many strategies can be sampled in finite time, any \(\overline{C}\) we compute may not be an overapproximation (as in 4); and by [rem:NoOverapprox], we cannot quantify the chance for this happening either. The fixed-budget algorithms thus focus on \(\underline{C}\), which they guarantee to be an underapproximation with probability \(\gamma\) again. They consist of a heuristic phase that determines a set of candidate strategies, followed by an evaluation phase that returns \(\underline{C}\). The latter samples new runs to ensure statistical independence between the phases to avoid bias (see 6 for an intuitive explanation). 5, the evaluation phase, is the same for WVR, FIB, and FSB; the heuristic phases differ, but all perform \(I \cdot m \cdot n\) simulation runs (up to rounding) for \(I\) a number of internal iterations. Our implementation then uses \(I \cdot m \cdot n\) more runs for the evaluation phase.

3.2.0.1 Weight vector refinement.

Listed in 6, our WVR algorithm implements the heuristic phase by linear scalarisation: it uses a specified number \(I\) of weight vectors to convert the multi-objective problem into \(I\) single-objective problems, as is done in multi-objective PMC, RL [67]–[69], and optimisation [70]–[72]. When determining the next weight vector, we pick the one with the largest distance between \(\underline{C}\) and \(\overline{C}\) (line [alg:weightvector:SelectW]) as in [19]. For each vector, we apply a round of smart strategy sampling [66] in lines [alg:weightvector:SSStart]-[alg:weightvector:SSEnd], with one exception: The worst-performing strategies are discarded from the local \(\Sigma'\) only, so that they will (temporarily) not receive more runs under the current weight vector. Every do loop iteration performs more runs for the remaining strategies to estimate the most promising ones (those with the highest value in the weight vector’s direction) most precisely.

Linear scalarisation is a necessity in PMC, to turn \(\phi\) into single-objective properties for which PMC algorithms are available. SMC, however, can estimate the values of multiple objectives at once, enabling more direct approaches:

3.2.0.2 Fixed iteration budget.

The FIB algorithm shown in 7 samples an initial set of strategies \(\Sigma_1\), then \(I\) times performs simulation runs for the current strategy set \(\Sigma_i\) (line [alg:fixediterationbudget:PerformSMC]) and heuristically discards unpromising strategies to form the next set \(\Sigma_{i+1}\) (line [alg:fixediterationbudget:Discard]). Each iteration evenly distributes \(m \cdot n\) runs over the strategies in \(\Sigma_i\), so that promising strategies are estimated ever more precisely.

3.2.0.3 Fixed strategy budget.

Instead of redistributing the budget for discarded strategies over the remaining strategies, FSB (shown in 8) samples new strategies so that, in the end, \(I \cdot n\) runs were performed for each ultimately surviving strategy. For multi-objective properties with many suboptimal strategies, this increases the probability of finding a Pareto-optimal strategy.

3.3 Strategy Selection Heuristics↩︎

We now describe our strategy selection heuristics, beginning with a simple rule:

Definition . \(\sigma\notin\mathsf{select\_candidates}_\mathit{simple}(\Sigma)\) iff there is a witness strategy \(\varsigma\in\Sigma\) such that, for all \(i \in \{\,1, \ldots, d\,\}\), \(\hat{x}_{i}^{\sigma} \leq \hat{x}_{i}^{\varsigma}\) if the \(i\)-th objective is maximising, and \(\hat{x}_{i}^{\sigma} \geq \hat{x}_{i}^{\varsigma}\) if it is minimising.

This rule effectively constructs a (non-convex) Pareto front from the sample means of the deterministic strategies in \(\Sigma\) as illustrated in [fig:rule:pareto-simple], discarding all strategies with suboptimal sample means: In the figure, \(\sigma\) will be discarded because witness \(\varsigma\) has a better sample mean.

The simple rule only compares sample means, not taking any statistical considerations into account. In [fig:rule:pareto-simple], the confidence boxes for \(\sigma\) and \(\varsigma\) overlap, so with the confidence level used, we cannot exclude that \(\sigma\) is in fact the better strategy. A more “precise” rule may decide to perform a probabilistic analysis and reject \(\sigma\) if it is “far enough” from the witness \(\varsigma\), where “far enough” means that the inequalities of [def:rule-simple] hold with sufficient probability. To simplify the process, we only consider CIs to define the criteria for rejection, not the full sample distributions, using the precisions of the CIs to establish “safe” distances.

[fig:all-rules] sketches all criteria we consider based on the sample means (dots) and confidence boxes for \(\sigma\) and witness \(\varsigma\); the double-ended arrows indicate the exclusion rules. Following the simple rule, all situations in [fig:all-rules] exclude \(\sigma\) as a consequence of the presence of \(\varsigma\). The more precise rules are defined as follows for maximising objectives; the criterion when minimising is the same with \(+\) and \(-\) as well as \(\leq\) and \(\geq\) switched:

The rules involving \(\varepsilon\) assume symmetric CIs, but extend analogously to asymmetric ones. Rule “far enough” (FE, [fig:all-rules:far-enough]) ensures that, for every objective, at least one of the values estimated with one strategy is outside the other strategy’s CIs. Strategy \(\varsigma\) cannot exclude \(\sigma\) in [fig:all-rules:simple] by this rule since \(\hat{x}_{2}^{\sigma}<\hat{x}_{2}^{\varsigma}+\min(\varepsilon_{2}^{\varsigma},\varepsilon_{2}^{\sigma})\), but it can do so in [fig:all-rules:far-enough] since \(\hat{x}_{1}^{\sigma}\leq\hat{x}_{1}^{\varsigma}-\varepsilon_{1}^{\varsigma}\) and \(\hat{x}_{2}^{\sigma}\geq\hat{x}_{2}^{\varsigma}+\varepsilon_{2}^{\sigma}\), and in all of [fig:all-rules:far-from-excluded,fig:all-rules:far-from-witness,fig:all-rules:far-from-each-other,fig:all-rules:conservatively-far].

The next rules focus on the confidence of one of the strategies: Rule “far from excluded” (FFE) requires the estimated values for witness \(\varsigma\) to be outside the CIs for the excluded strategy \(\sigma\), shown in [fig:all-rules:far-from-excluded]. Dual to this is “far from witness” (FFW), shown in [fig:all-rules:far-from-witness]. These two rules are incomparable but implied by “simple” and “far enough”. The intersection of both rules is “far from each other” (FFEO), visualised in [fig:all-rules:far-from-each-other]. This rule also excludes \(\sigma\) in the situation of [fig:all-rules:conservatively-far], but will not exclude it in the situations of [fig:all-rules:simple,fig:all-rules:far-enough,fig:all-rules:far-from-excluded,fig:all-rules:far-from-witness]. The final and most conservative rule is “conservatively far” (CF), which ensures that the CIs obtained with the excluded strategy \(\sigma\) do not overlap with the CIs obtained with the witness \(\varsigma\) as shown in [fig:all-rules:conservatively-far].

4 Experimental Evaluation↩︎

We implemented the algorithms and heuristics of 3 in modes to experimentally study their effectiveness and performance. Our implementation follows the given pseudocode, except that in the fixed-budget algorithms, any budget unused due to rounding effects in one iteration is carried over to the next.

4.1 Benchmark Set↩︎

We compiled a representative benchmark set consisting of benchmarks from PMC and RL. For the former, we use all multi-objective models from [37] that modes supports (in terms of modelling features) and that have nontrivial Pareto fronts (i.e. of more than one Pareto-optimal point, as computed via PMC). These models are small enough to be checked with PMC. To demonstrate that our approaches keep working when PMC starts to struggle with state space explosion and higher dimensions, we also consider models commonly used in RL literature [73]–[76]: (1) the breakable bottles model [77] with 3 objectives, (2) the fruit tree model [78] with both 2 and 6 objectives, (3) deterministic and probabilistic versions of the deep sea treasure case [79], and (4) racetrack benchmarks [80], which we make multi-objective via the puddle world [81] reward scheme. For details, see 8. Altogether, we end up with 15 models. Most are parametrised; we consider up to three different parameter valuations per model and one multi-objective property, giving us a final set of 40 benchmark instances. The benchmark selection was done prior to running any experiments, and was not based on any expectations of the performance of our approaches.

4.2 Experimental Setup↩︎

To be able to assess the impact of the number of initial strategies \(m\) and the run count parameter \(n\) on the fixed-budget algorithms, we use three different

r3.7cm

2.5pt

configurations as listed in 1, and evaluate each algorithm on each instance with all heuristics in all configurations, leading to \(3 \cdot 40 \cdot 6 \cdot 3 = 2160\) different experiments. WVR samples \(\frac{m}{2}\), FIB \(m\), and FSB at most \(\approx m \cdot \ln I\) strategies. We thus sample \(<10000\), so much fewer than \(2^{32}\), strategies in each experiment.

We judge each setting by its result’s hypervolume (HV) [82]: the area under the Pareto front with respect to a “worst possible” reference point. In [fig:ExampleCurveApproximation], a reasonable reference point is the top left corner; then the HV of the underapproximation is the extent of the visible blue (top left) area. The HV is the only known metric that is strictly monotonic [83], meaning that if one approximation strictly contains another, its HV will be larger. This makes it popular in multi-objective research [84]–[87], but a disadvantage is that the reference point is arbitrary. Thus the HV is useful for a qualitative comparison of results on the same model, but not across different models or for a quantitative evaluation.

To quantify the quality of an approximation w.r.t.a reference Pareto front/achievable set, we compute the multiplicative \(\epsilon\) [83] of the underapproximation. This metric is the least factor by which each point in an approximation should be scalar-multiplied (or divided in case of a minimising objective) in order to be a superset of the reference. A multiplicative \(\epsilon\) of \(1\) means that the approximation already fully contains the reference set and is thus optimal. Infinite multiplicative \(\epsilon\) values can arise when a minimising property needs to approximate the actual value \(0\): for a value \(x \neq 0\), observe that only \(\lim_{a \rightarrow \infty} \frac{x}{a} = 0\). Since the multiplicative \(\epsilon\) only considers the worst-performing point of the approximation, it can—and in our benchmarks does—happen that two approximations have equal multiplicative \(\epsilon\) but one is a superset of the other. Improvements in the rest of the approximation beyond the worst point can only be captured using the HV.

We run each experiment three times, each with a different strategy seed (of \(1\), \(2\), and \(3\)). We report the average of the three HVs, and of the multiplicative \(\epsilon\)s if a reference front/set is known (either from insights into the model, or obtained via PMC). We ran our experiments on a 64-bit Ubuntu Linux 22.04 system with AMD Ryzen 9 7950X3D CPU (4.2-5.7 GHz) and 128 GB of RAM.

4.3 Comparison with PMC↩︎

2.5pt

2 first lists the number of objectives in the property and the number of states of the MDP for each benchmark instance. The latter has been computed via PMC (using Storm in exact mode where possible, otherwise approximated via mcsta’s [88] new sound multi-objective PMC implementation [59] and marked *) or, if that failed, estimated by the authors from model-specific insights (marked **). It then compares the Pareto fronts—obtained via PMC (assumed to be correct and taken as the reference) or manually from model insights—with those approximated by our approaches, and the corresponding runtimes: “PMC time” is the runtime of Storm or mcsta, or a timeout “TO” (\(>1\) hour). Column “our time” gives the interval from lowest to highest runtime of our approaches over all \(3 \cdot 6 \cdot 3\) experiments performed per instance (\(\text{TO} > 10\) minutes), while the last column contains analogous intervals over the multiplicative \(\epsilon\)s.

We see that the PMC tools run out time on the larger RL benchmarks, while all our fixed-budget experiments succeed, often in seconds. The SMC-based Pareto front underapproximations can get fairly close to the true Pareto fronts in this time, as observed for the deep_sea and fruit_tree models, but may also be quite far off as observed for the breakable_bottles model.

4.4 Fixed-Budget Algorithms Comparison↩︎

We compare the fixed-budget algorithms and heuristics in terms of HV. Each experiment performs a similar number of simulation runs, but wall-clock runtimes may differ due to per-strategy overhead in modes and because some strategies induce longer runs.

r6.25cm

2pt

4.4.0.1 Best algorithm, heuristic, and configuration.

No one combination of configuration, heuristic, and algorithm always wins, as shown in 3, where we list the number of models on which each combination outperformed all other combinations (i.e. delivered the highest HV, over the whole table). FSB performs best overall. The total count is \(37\) instead of \(40\) since the experiments timed out on care_home and resource_gathering, while there is no unique best combination for the deep_sea_probabilistic.5-100 instance.

The heuristics significantly influence the number of strategies surviving each iteration. To evaluate their effect on each of the fixed-budget algorithms, we show in ¿tbl:tab:results:heuristics? the number of models for which each heuristic outperformed all others per algorithm (i.e. within a column). The simple strategy obtains the highest HV for most algorithms. It thus appears that it is often beneficial (in our benchmark set) to discard strategies that do not look promising as early as possible and distribute the remaining budget over other strategies, although as observed in 3, other heuristics might lead to better overall results.

¿tbl:tab:results:config? shows the number of models for which each configuration from 1 performs best for each heuristic-algorithm pair (i.e. in a 3-column block within a row). On these benchmarks, configuration \(3\) performs best in almost every case, with the exception of the conservatively-far heuristic. This heuristic needs the intervals to be smaller to discard suboptimal strategies and thus requires more simulation runs. For the other approaches, it appears that having more, and thus presumably a wider variety of, strategies is more important than evaluating each strategy more precisely.

4.4.0.2 Strategies per iteration.

The number of strategies remaining in each iteration naturally differs between the algorithms as illustrated for a deep_sea and a fruit_tree instance using the simple heuristic in 10. In the deep_sea model, most sampled strategies are suboptimal, whereas in the fruit_tree model, most strategies are close to Pareto-optimal. When most strategies are determined to be suboptimal, the FIB algorithm instantly discards most strategies. FSB does the same, but uses the remaining budget to sample new strategies. WVR, in contrast, only drops strategies after the last iteration.

4.4.0.3 Strategy seeds.

As stated previously, each experiment was run with three different strategy seeds. The reason for doing so can be seen in the underapproximations for the three different seeds for one of the racetrack-puddle world models in 11: Even though the model, algorithm, heuristic, and configuration are the same, there is still a significant difference in the computed underapproximations.

4.5 The Incremental Scheme↩︎

The effect of the incremental scheme’s parameters can be seen without running experiments, as in [fig:approximation-settings:middle]. Nevertheless, we experimentally inspect the underapproximations it finds, which we show for the deep sea treasure model and different timeouts in [fig:incremental:deep-sea]. As expected, better strategies are sampled over time, and the approximation closes in on the true Pareto front.

Many more plots from our experiments, in particular visualisations like [fig:ParetoFrontExtendedExample] of the Pareto fronts found via our SMC-based approaches, are in 9.

5 Conclusion↩︎

We introduced the first multi-objective SMC approach that (i) addresses the general case of \(d\) equal-priority probabilistic objectives and (ii) is constant-memory w.r.t. the model’s state space size. Our algorithms approximate the achievable set and Pareto front. They provide statistical guarantees on the underapproximation, and the incremental approach also comes with a limit guarantee for the overapproximation. Our experiments indicate that, in finite time, the fixed strategy budget algorithm with the simple heuristic, a high number of initial strategies, and a small number of runs for each tends to perform best.

Our approach directly applies to models beyond MDP for which single-objective LSS is available. It also extends to infinite-state models in principle, as long as runs almost surely terminate; however, the overapproximation in the incremental approach would no longer converge because we could no longer assume every strategy to eventually be sampled given fixed-size strategy identifiers.

5.0.0.1 Data availability.

The exercised versions of modes and Storm, benchmarks, produced results, and a docker environment are available on Zenodo [89].

6 Additional Explanations↩︎

To explain the need for generating new runs in the evaluation phase of our fixed-budget algorithms (as described on page ), let us make an analogy: Consider the experiment of tossing \(100\) fair coins \(n\) times, and let us repeat it \(1000000\) times. If we (i) discard all experiments but the one with the highest rate of getting heads, and then (ii) use the already-collected data for that experiment to get a \(95\,\%\) CI based on \(n\) runs for that coin’s probability of showing heads, we are much more likely than \(95\,\%\) to falsely conclude that the coin is biased. We thus need to collect new samples for (ii), or apply Bonferroni correction to divide the error budget over all \(1000000\) repetitions to achieve simultaneous \(95\,\%\) confidence. The former needs \(n\) extra runs, while (using the Okamoto bound [90]) the latter now needs \(10^6\cdot n\) in each repetition, so just below \(10^{11}\cdot n\) extra runs in total.

7 Additional Figures and Plots↩︎

12 provides two additional views on the tradeoffs in 3 (the incremental scheme) that are further zoomed out ([fig:approximation-settings:large]) and further zoomed in ([fig:approximation-settings:small]) compared to [fig:approximation-settings:middle] in 3.1.

8 Details on Benchmark Models↩︎

We provide more details on the families of benchmark models that we added over the ones collected from QComp 2023 to demonstrate that our algorithms can analyse models that PMC struggles with.

8.0.0.1 Breakable bottles.

The breakable bottles model [77] represents a person that wants to move bottles from position A to position B. However, if they carry more than one bottle at a time, with each movement there is a 10 % chance of dropping, and thereby breaking, one bottle. At some point, the person will get exhausted from all of this exercise and has to stop. There are three rewards, representing (1.) the number of broken bottles, (2.) the number of successfully transferred bottles, and (3.) the number of steps taken.

8.0.0.2 Deep sea treasure.

The deep sea treasure model [79] is commonly used in RL [73], [91]–[94]. In this model, a deep sea submarine searching for treasure is controlled. Larger treasures are located deeper underwater, which introduces trade-off with fuel consumption. We use two variants of this model: a deterministic and a probabilistic version. The original deep sea treasure model is deterministic, which allows for a straightforward computation of the correct Pareto front [79]. To make it more interesting, we use a larger environment than the original model, which makes it challenging for PMC. The probabilistic version introduces a probabilistic chance of the submarine imploding when it submerges too quickly, thus requiring greater patience.

8.0.0.3 Fruit tree model.

The fruit tree model [78] is a perfect binary tree with each leaf handing out rewards corresponding to nutrients of the fruit on that leaf. To obtain non-trivial Pareto fronts, the reward vector with 2 objectives is chosen such that each leaf corresponds to a discrete point in the positive quadrant of the quadratic equation \(1 - x^2\). For 6 objectives, each leaf corresponds to a discrete point on the all-positive section of a 5-sphere. Since each state corresponds to two new states in the next depth, the state space grows exponentially. Since the state space explodes rapidly, these models are computationally infeasible for PMC. However, the length of the paths scales linearly with depth, making these models suitable for SMC.

8.0.0.4 Puddle world racetracks.

We finally include racetrack benchmarks [80], which are also used in AI literature [74], [95]–[97] and have been adopted by the PMC community as well [98]–[100]. In these models, the driver must select a direction in which they would like to accelerate at every timestamp. The car then has a 90 % chance of accelerating in that direction. The driver aims to optimise the probability of reaching the finish line without leaving the track. To make them multi-objective, we use the classic puddle world [81] reward scheme, which is widely used in RL literature [75], [76], [101]–[103]. In the puddle world, the agent aims to finish as soon as possible but would like to avoid the puddles, which are the off-track areas of the map. Since the path to the finish is shorter when driving off-track, there is a trade-off between the puddle punishment and the time to reach the finish line.

9 Additional Experimental Results↩︎

We provide some more plots to illustrate our findings. For each model, we provide a plot analogous to 11 of the three seeds, using FSB, the simple heuristic, and configuration 3 since we found in 4 that those performed best overall. The results are shown in [app:fig:deep_sea,app:fig:deep_sea_probabilistic,app:fig:energy_aware_scheduling,app:fig:fruit_tree_2,app:fig:mars_rover,app:fig:puddle_world_barto_big,app:fig:puddle_world_barto_small,app:fig:puddle_world_hansen,app:fig:puddle_world_ring,app:fig:puddle_world_river,app:fig:puddle_world_tiny]; the true Pareto front is shown in black in case it is known.

The true Pareto fronts are known by construction for the fruit-tree, deep-sea (both variants) and breakable-bottles models. For the large fruit-tree there are too many Pareto-optimal points to feasibly compute the multiplicative epsilon.

In the breakable-bottles model, a Pareto-optimal strategy is to only walk with one bottle from A to B and back. The probability of finding this strategy, or a very close one, is low. Hence, this model serves as an example of when our approach is not suitable (but we did not select it for this purpose a priori).

References↩︎