360
F. Delgrange et al.
Table 1: Results for stationary strategies.
BenchInstance 1
ε=0.01 ε=0.001
Instance 2
ε=0.01 ε=0.001
mark Par. |S| %E Act Time |P | Time |P | Par. |S| %E Act Time |P | Time |P |
dpm 2
∗
2
1272 32 3.2
17 37 315 377
3
1696 30 3.2
82 30
TO
eajs
2
∗
2-3
689 0 1.2
5 23
45 202 3-6 2·10
4
0 1.2 201 52 3787 375
jobs 3
∗
3-2
17 0 1.1
3 3
2 3 5-2
117 0 1.5 2042 76
TO
mutex 3
∗
1
1795 36 2.2
TO
TO
2 1·10
4 33 2.3
TO
TO
polling 2
2-2
233 86 1.5
6 5
23 6 3-2
990 84 1.8 299 5
TO
rg
2
∗ 2-1-20 2173 14 2.9
5 5
12 5 5-2-50 3·10
4
5 3.1 496 27
TO
rover 2
∗ 2500 2·10
4
0 1.2 110 47 417 251 5000 4·10
4
0 1.2 258 47 3105 472
serv
2
∗
5·10
4 93 1.9 1828 38
TO
str
2
∗
30 1426 0 1.3
11 21 822 218 500 4·10
5
0 1.3 2428 17
TO
team2 2
∗
2
1847 24 1.2
2 5
2 5
3 1·10
4 21 1.2
18 43
MO
team3 3
∗
2
1847 24 1.2 165 15 166 15
3 1·10
4 21 1.2
TO
TO
uav
2
∗
750 2·10
5 29 1.6 400 39 5799 332 1000 4·10
5 31 1.8 3546 36
TO
wlan 2
∗
0
2954 0 1.3 160 16
TO
2 3·10
4
0 1.3 6728 23
TO
The pure bounded Pareto approximation problem is defined similarly. We reduce
a PBMA instance to an instance for PSMA. The idea is to incorporate a memory
structure of size K into M and then construct a pure stationary strategy in this
product MDP (see, e.g., [29] for a similar construction). The set of strategies
can be further refined by considering e.g., a memory structure that only allows
counting or that only remembers visits of goal states. See [17, App. D] for details.
6 Evaluation
We implemented our approach for PSP
≈ in the model checker Storm [16] using
Gurobi [27] as back end for MILP-solving. The implementation takes an MDP
(e.g., in Prism syntax), a multi-objective query, and a precision ε > 0 as input
and computes an -approximation of the Pareto front. Here, we set j = ε · δ j ,
where δ j is the difference between the maximal and minimal achievable value for
objective ψ j . We also support reward objectives for Markov automata via [38].
The computations within Gurobi might suffer from numerical instabilities. To
diminish their impact, we use the exact engine of Storm to confirm for each
MILP solution that the encoded strategy achieves the encoded point. However,
sub-optimal solutions returned by Gurobi may still yield inaccurate results.
We evaluate our approach on 13 multi-objective benchmarks from [24,28,38],
each considering one or two parameter instantiations. Application areas range
over scheduling (dpm [37], eajs [1], jobs [10], polling [43]), planning (rg [6], rover [28],
serv [32], uav [21]), and protocols (mutex [38], str [38], team [15], wlan [31]).
The results for pure stationary strategies are summarized in Table 1. For each
benchmark we denote the number of objectives and whether the alternative
encoding from Sect. 3.4 has been applied (
∗ ). For each parameter instantiation
(Par.), the number of states (|S|), the percentage of the states that are contained
in an end component (%E), and the average number of available actions at each
state (Act ) are given. For each precision ε ∈ {0.01, 0.001}, we then depict the
F. Delgrange et al.
Table 1: Results for stationary strategies.
BenchInstance 1
ε=0.01 ε=0.001
Instance 2
ε=0.01 ε=0.001
mark Par. |S| %E Act Time |P | Time |P | Par. |S| %E Act Time |P | Time |P |
dpm 2
∗
2
1272 32 3.2
17 37 315 377
3
1696 30 3.2
82 30
TO
eajs
2
∗
2-3
689 0 1.2
5 23
45 202 3-6 2·10
4
0 1.2 201 52 3787 375
jobs 3
∗
3-2
17 0 1.1
3 3
2 3 5-2
117 0 1.5 2042 76
TO
mutex 3
∗
1
1795 36 2.2
TO
TO
2 1·10
4 33 2.3
TO
TO
polling 2
2-2
233 86 1.5
6 5
23 6 3-2
990 84 1.8 299 5
TO
rg
2
∗ 2-1-20 2173 14 2.9
5 5
12 5 5-2-50 3·10
4
5 3.1 496 27
TO
rover 2
∗ 2500 2·10
4
0 1.2 110 47 417 251 5000 4·10
4
0 1.2 258 47 3105 472
serv
2
∗
5·10
4 93 1.9 1828 38
TO
str
2
∗
30 1426 0 1.3
11 21 822 218 500 4·10
5
0 1.3 2428 17
TO
team2 2
∗
2
1847 24 1.2
2 5
2 5
3 1·10
4 21 1.2
18 43
MO
team3 3
∗
2
1847 24 1.2 165 15 166 15
3 1·10
4 21 1.2
TO
TO
uav
2
∗
750 2·10
5 29 1.6 400 39 5799 332 1000 4·10
5 31 1.8 3546 36
TO
wlan 2
∗
0
2954 0 1.3 160 16
TO
2 3·10
4
0 1.3 6728 23
TO
The pure bounded Pareto approximation problem is defined similarly. We reduce
a PBMA instance to an instance for PSMA. The idea is to incorporate a memory
structure of size K into M and then construct a pure stationary strategy in this
product MDP (see, e.g., [29] for a similar construction). The set of strategies
can be further refined by considering e.g., a memory structure that only allows
counting or that only remembers visits of goal states. See [17, App. D] for details.
6 Evaluation
We implemented our approach for PSP
≈ in the model checker Storm [16] using
Gurobi [27] as back end for MILP-solving. The implementation takes an MDP
(e.g., in Prism syntax), a multi-objective query, and a precision ε > 0 as input
and computes an -approximation of the Pareto front. Here, we set j = ε · δ j ,
where δ j is the difference between the maximal and minimal achievable value for
objective ψ j . We also support reward objectives for Markov automata via [38].
The computations within Gurobi might suffer from numerical instabilities. To
diminish their impact, we use the exact engine of Storm to confirm for each
MILP solution that the encoded strategy achieves the encoded point. However,
sub-optimal solutions returned by Gurobi may still yield inaccurate results.
We evaluate our approach on 13 multi-objective benchmarks from [24,28,38],
each considering one or two parameter instantiations. Application areas range
over scheduling (dpm [37], eajs [1], jobs [10], polling [43]), planning (rg [6], rover [28],
serv [32], uav [21]), and protocols (mutex [38], str [38], team [15], wlan [31]).
The results for pure stationary strategies are summarized in Table 1. For each
benchmark we denote the number of objectives and whether the alternative
encoding from Sect. 3.4 has been applied (
∗ ). For each parameter instantiation
(Par.), the number of states (|S|), the percentage of the states that are contained
in an end component (%E), and the average number of available actions at each
state (Act ) are given. For each precision ε ∈ {0.01, 0.001}, we then depict the