338
F. Funke et al.
(a) Witnesses for Pr
min
s 0 (♦ goal) ≥ λ.
(b) Witnesses for Pr
max
s 0 (♦ goal) ≥ λ.
Fig. 4: MDP benchmark: consensus-2-4 (528 states)
In Figure 3 it can be seen that the QS heuristics derived from the two polytopes
P
max and P
min
≥0 may produce different results. However, for both models one of
them gives monotonically growing subsystems and outperforms Comics. While
QS 2 applied to P
min
≥0 performs better on crowds-5-8 (Figure 3a), it is the other
way around on brp-512-2 (Figure 3b). In future work we intend to investigate
what properties determine which of the two formulations performs better for a
given DTMC.
MDP benchmarks. We consider two MDP models: the randomized consensusN -K protocol of [10, 60] (with N processes and a bound K on the random walk)
and the CSMA-N -K protocol for data channels [61] (where N is the number of
stations, and K is the maximal backoff count). The results of both heuristic and
exact computations can be seen in Figure 4 and Figure 5. Whereas the heuristics
all needed less than 5 minutes, all MILP instances ran into the timeout except for
the ones in Figure 4a. Whenever a MILP instance could not be solved optimally
in 30 minutes, we plot both the found upper and lower bound, with the region in
between shaded. It should be noted that the condition Pr
min (♦(goal ∨ fail)) holds
for the instances of these models, and reachability properties, that we consider.
The comparison between the MILP formulation that we derived from P
max (λ)
and the one presented in [77, 78] (labeled by ltlsubsys, see also Section 6)
shows that both compute comparable upper and lower bounds in Figure 4b,
whereas ltlsubsys found worse upper bounds in Figure 5b. In all instances
apart from Figure 4b the corresponding QS 2 heuristics performs well and generates subsystems that are as good, or better, than the best upper bounds
computed by the MILPs in 30 minutes. As expected, the witnessing subsystems
for Pr
min
s0 (♦ goal) ≥ λ tend to the entire state space as λ tends to the actual
value Pr
min
s0 (♦ goal) (which is 1 in these two models). However, subsystems for
Pr
max
s0 (♦ goal) ≥ λ may be substantially smaller even for large λ.
F. Funke et al.
(a) Witnesses for Pr
min
s 0 (♦ goal) ≥ λ.
(b) Witnesses for Pr
max
s 0 (♦ goal) ≥ λ.
Fig. 4: MDP benchmark: consensus-2-4 (528 states)
In Figure 3 it can be seen that the QS heuristics derived from the two polytopes
P
max and P
min
≥0 may produce different results. However, for both models one of
them gives monotonically growing subsystems and outperforms Comics. While
QS 2 applied to P
min
≥0 performs better on crowds-5-8 (Figure 3a), it is the other
way around on brp-512-2 (Figure 3b). In future work we intend to investigate
what properties determine which of the two formulations performs better for a
given DTMC.
MDP benchmarks. We consider two MDP models: the randomized consensusN -K protocol of [10, 60] (with N processes and a bound K on the random walk)
and the CSMA-N -K protocol for data channels [61] (where N is the number of
stations, and K is the maximal backoff count). The results of both heuristic and
exact computations can be seen in Figure 4 and Figure 5. Whereas the heuristics
all needed less than 5 minutes, all MILP instances ran into the timeout except for
the ones in Figure 4a. Whenever a MILP instance could not be solved optimally
in 30 minutes, we plot both the found upper and lower bound, with the region in
between shaded. It should be noted that the condition Pr
min (♦(goal ∨ fail)) holds
for the instances of these models, and reachability properties, that we consider.
The comparison between the MILP formulation that we derived from P
max (λ)
and the one presented in [77, 78] (labeled by ltlsubsys, see also Section 6)
shows that both compute comparable upper and lower bounds in Figure 4b,
whereas ltlsubsys found worse upper bounds in Figure 5b. In all instances
apart from Figure 4b the corresponding QS 2 heuristics performs well and generates subsystems that are as good, or better, than the best upper bounds
computed by the MILPs in 30 minutes. As expected, the witnessing subsystems
for Pr
min
s0 (♦ goal) ≥ λ tend to the entire state space as λ tends to the actual
value Pr
min
s0 (♦ goal) (which is 1 in these two models). However, subsystems for
Pr
max
s0 (♦ goal) ≥ λ may be substantially smaller even for large λ.