336
F. Funke et al.
initial state to goal, and adds it to the subsystem. Both approaches iteratively
extend a subsystem until it carries more probability than the given threshold
and thus have to compute the probability of the subsystem at each iteration.
All computations were performed on a computer with two Intel E5-2680 8
cores at 2.70 GHz running Linux, with a time bound of 30 minutes, a memory
bound of 100 GB and with each benchmark instance having access to 4 cores.
For the LP and MILP instances we use the Gurobi solver, version 8.1.1 [43]. The
recorded times of our computations include the construction of the LPs/MILPs
and are wall clock times. Pre-processing steps, such as collapsing states that
cannot reach goal, are not counted in the time consumption. For Comics, we
use the time that is reported as counterexample generation time by the tool.
To validate our implementation, we used Prism to verify that the subsystems
that we compute indeed satisfy the probability thresholds. We noticed that for a
few instances (< 0.5%) Prism reported a deviation of less than 10
−8 , which can
be explained by the fact that both Prism and the solvers that we use rely on
floating-point arithmetic, which is approximate by nature.
Our implementation, together with the models we use and benchmark results
can be found at https://github.com/simonjantsch/farkas.
(a) QS-heuristic applied to P
max (λ).
(b) QS-heuristic applied to P
min
≥0 (λ).
Fig. 2: crowds-2-8: comparing QS k for growing k.
DTMC benchmarks. As Pr
max and Pr
min coincide on DTMCs, we can use
the heuristics and exact computations derived from either the P
max or the P
min
≥0
polytope for DTMCs (in Comics we use the standard query Pr s0 (♦ goal) ≥ λ).
We consider two DTMC benchmarks: a model of the crowds-N -K protocol [69, 72]
for ensuring anonymous web browsing (with N members and K protocol runs)
and a model of the bounded retransmission protocol [34, 47] for file transfers
(where brp-N -K is the instance with N chunks and K retransmissions).
F. Funke et al.
initial state to goal, and adds it to the subsystem. Both approaches iteratively
extend a subsystem until it carries more probability than the given threshold
and thus have to compute the probability of the subsystem at each iteration.
All computations were performed on a computer with two Intel E5-2680 8
cores at 2.70 GHz running Linux, with a time bound of 30 minutes, a memory
bound of 100 GB and with each benchmark instance having access to 4 cores.
For the LP and MILP instances we use the Gurobi solver, version 8.1.1 [43]. The
recorded times of our computations include the construction of the LPs/MILPs
and are wall clock times. Pre-processing steps, such as collapsing states that
cannot reach goal, are not counted in the time consumption. For Comics, we
use the time that is reported as counterexample generation time by the tool.
To validate our implementation, we used Prism to verify that the subsystems
that we compute indeed satisfy the probability thresholds. We noticed that for a
few instances (< 0.5%) Prism reported a deviation of less than 10
−8 , which can
be explained by the fact that both Prism and the solvers that we use rely on
floating-point arithmetic, which is approximate by nature.
Our implementation, together with the models we use and benchmark results
can be found at https://github.com/simonjantsch/farkas.
(a) QS-heuristic applied to P
max (λ).
(b) QS-heuristic applied to P
min
≥0 (λ).
Fig. 2: crowds-2-8: comparing QS k for growing k.
DTMC benchmarks. As Pr
max and Pr
min coincide on DTMCs, we can use
the heuristics and exact computations derived from either the P
max or the P
min
≥0
polytope for DTMCs (in Comics we use the standard query Pr s0 (♦ goal) ≥ λ).
We consider two DTMC benchmarks: a model of the crowds-N -K protocol [69, 72]
for ensuring anonymous web browsing (with N members and K protocol runs)
and a model of the bounded retransmission protocol [34, 47] for file transfers
(where brp-N -K is the instance with N chunks and K retransmissions).