Farkas certificates and minimal witnesses
337
(a) crowds-5-8 (46,873 states). Comics-global runs out of memory for λ ≥ 0.23.
(b) brp-512-2 (15,875 states). Comics-local reports an error for λ ≥ 2.1 · 10
−5 and
Comics-global runs out of memory for λ = 2.6 · 10
−5 .
Fig. 3: Comparison of heuristic methods on DTMC benchmarks.
Figure 2 shows the effect of increasing the number of iterations of the QSheuristic for the model crowds-2-8. While the first iteration (taking QS 2 instead
of QS 1 ) has an impact on the number of states, more iterations do not improve
the result significantly. For QS 1 , the sizes of subsystems increase monotonically
with growing λ. Starting with QS 2 the results may, interestingly, have “spikes”:
increasing λ can lead to smaller subsystems.
Figure 3 shows the results of the QS 2 -heuristic compared to the two modes
of Comics for λ that ranges between 0 and the actual reachability probability
of the model. A general observation is that the runtime of the QS-heuristic is
independent of λ, whereas both modes of Comics use significantly more time
with increasing λ. The same observation can be done for memory consumption,
which stayed below 200 MB for our heuristics. Also, especially for crowds-5-8,
one can see that relatively small subsystems are possible even for large λ. The
exact computations via MILPs hit the timeout for almost all instances.
337
(a) crowds-5-8 (46,873 states). Comics-global runs out of memory for λ ≥ 0.23.
(b) brp-512-2 (15,875 states). Comics-local reports an error for λ ≥ 2.1 · 10
−5 and
Comics-global runs out of memory for λ = 2.6 · 10
−5 .
Fig. 3: Comparison of heuristic methods on DTMC benchmarks.
Figure 2 shows the effect of increasing the number of iterations of the QSheuristic for the model crowds-2-8. While the first iteration (taking QS 2 instead
of QS 1 ) has an impact on the number of states, more iterations do not improve
the result significantly. For QS 1 , the sizes of subsystems increase monotonically
with growing λ. Starting with QS 2 the results may, interestingly, have “spikes”:
increasing λ can lead to smaller subsystems.
Figure 3 shows the results of the QS 2 -heuristic compared to the two modes
of Comics for λ that ranges between 0 and the actual reachability probability
of the model. A general observation is that the runtime of the QS-heuristic is
independent of λ, whereas both modes of Comics use significantly more time
with increasing λ. The same observation can be done for memory consumption,
which stayed below 200 MB for our heuristics. Also, especially for crowds-5-8,
one can see that relatively small subsystems are possible even for large λ. The
exact computations via MILPs hit the timeout for almost all instances.