Case Studies
Below are a number of case studies conducted
using INFAMY
. Most of them are variants of
case studies from the PRISM
homepage. All of them are
based on them described in
the publications section. The results were obtained on
a Linux machine with an AMD Athlon^{TM} XP 2600+ processor
at 2 GHz equipped with 2 GB of RAM. Where convenient, we denote
multiples of thousand by "K".
 Random Walk
 Jackson Queuing Networks
 QuasiBirthDeath Processes
 Protein Synthesis
 GridWorld Robot
 Tandem Queueing Network
 Workstation cluster
Random Walk
We consider a discretespace, continuoustime random walk model, in which a walker starts from the initial position 0, and changes position with rate λ. The field directly left to the current position is chosen with a probability of p, and the field to the right with a probability of 1p. We consider two properties:
 an instantaneous reward property: the expected distance from the starting point at a given point in time
 a probabilistic reachability property: the probability that the walker moves at least 10 fields to the right within a certain time bound t, expressed by P_{=?} (♢^{≤t} m≥10) where m denotes the position of the walker.
The corresponding results for p=0.25, and λ=1 are given in the table below. For the truncation, a precision of 10^{6} was used. Here, the analysis time given is only for analyzing the first property after statespace exploration. The time with respect to the second property is in the same order as the first one. As apparent from the data, the size of the model is approximately proportional to the depth and the time bound t. The Layeredchain and FSP configurations achieve consistently smaller truncation depths than Uniform. Due to the simple structure of the model, however, FSP turns out to be slower than the Uniform and Layered chain configurations. This is because, for the FSP configuration, the transient analysis for state exploration consumes a proportionally high amount of time, especially for large time bounds t.
t  Uniform  Layered  FSP  exp.  prob.  

dep  time (s)  n  dep  time (s)  n  dep  time (s)  n  
50  223  0.9/0.0  447  71  0.9/0.0  143  62  0.9/0.0  125  2.50E+01  0.99 
100  273  0.9/0.0  547  121  0.9/0.0  243  101  1.0/0.0  203  5.00E+01  1.00 
1K  1.3K  0.9/0.1  2.5K  885  0.9/0.1  1.8K  654  16.3/0.0  1.3K  5.00E+02  1.00 
5K  5.6K  0.9/1.8  11.2K  4.0K  1.2/1.2  8.1K  2.8K  1,462/0.7  5.7K  2.50E+03  1.00 
Jackson Queuing Networks
A Jackson Queuing Network (JQN) [Jackson57] is a system consisting of a number of n interconnected queuing stations. A JQN with two queues is depicted in the figure below.
Jobs arrive from the environment with a negative exponential interarrival time and are distributed to station i with probability r_{0,i}. Each station is connected to a single server which handles the jobs with a service time given by a negative exponential distribution with rate μ_{i}. Jobs processed by the station of queue i leave the system with probability r_{i,0} but are put back into queue j with probability r_{i,j}. JQNs have an infinite state space because the queues are unbounded. Initially all queues are empty. In this paper, we consider JQN models with N=3,4,5 queues. The arrival rate for N queues is λ, which is then distributed to station j (with service rate μ_{j}:=j) with probability μ_{j}/(∑_{i=1}^{N}μ_{i}). The probability out of a service rate is then uniformly distributed. We compute the probability that, within t=10 time units, a state is reached in which 4 or more jobs are in the first and 6 or more jobs are in the second queue.
N/λ  Uniform  Layered  FSP  prob.  

dep  time  n  dep  time  n  dep  time  n  
3 / 2  193  8/19  1,236K  46  1/1  18K  37  4/0  10K  1.98E01 
4 / 2        46  3/11  230K  35  43/4  82K  1.20E01 
5 / 2        46  37/187  2,349K  34  392/50  576K  8.94E02 
3 / 3  203  10/23  1,436K  60  1/1  40K  51  14/1  25K  5.90E01 
4 / 3        60  7/27  635K  48  202/13  271K  4.42E01 
5 / 3              46  2,299/193  2,349K  3.71E01 
3 / 4  212  12/26  1,633K  74  1/2  73K  64  35/1  48K  8.38E01 
4 / 4        74  15/55  1,426K  61  665/29  677K  7.16E01 
3 / 5  223  13/31  1,898K  88  2/3  121K  77  76/2  82K  9.43E01 
4 / 5        88  30/101  2,794K  74  1,772/58  1,426K  8.65E01 
Results for different number of queues N and arrival rate λ are given in the table above. For the truncation, a precision of 10^{6} was used. Observe that, for fixed arrival rate λ, the depth is insensitive to the number of queues in Layered and Uniform configurations. The service rate increases with N, however, transitions corresponding to the service rate only lead back to states which are already explored, thus not contributing to the forward exit rates. For FSP, the depth is smaller than the Layered chain configuration. The number of states, and also the number of transitions, grow very fast with respect to the depth. Uniform chain cannot handle the cases N=4,5, as opposed to the other two configurations. While in the Layered chain configuration the dominating part is the model checking time in the truncation, the dominating part of the FSP configuration is the state exploration part. For N=5 and λ=3;, it is the only configuration that still works.
If the truncation grows very fast with respect to the depth, an approach that combines the two configurations might be the only option for large N and λ. Such an approach is left for future work.
QuasiBirthDeath Processes
In [KatoenKLW07], a case study is considered that describes a system consisting of a fixed number of m processors and an infinite queue for storing job requests. The processing speed of a processor is described by the rate γ, while λ describes the incoming rate of new jobs. If a new job arrives while at least one processor is idle, the job will be processed directly. Otherwise, it will be put into a waiting queue. If there are idle processors and the waiting queue is nonempty, a job will be taken from the queue and processed immediately. To model this spontaneous transition, a rate μ >> λ is used. The stochastic Petri net (SPN) used in [KatoenKLW07]is depicted in the figure below for the case m=3.
Tokens in place p_{1} represent the number of idle processors, place p_{2} describes the number of busy processors and place p_{3} gives the number of jobs in the queue. Transition t_{1} models the case of an incoming job given that at least one processors is idle, whereas t_{4} describes the case in which all processors are busy, thus the job is put into the queue. Transition t_{2} represents the successful termination of a job. Finally, t_{3} is the spontaneous transition in case there are idle processors and the queue is nonempty. We consider the probability that, given that all processors are busy and there are no jobs in the queue, within t time units a state will be reached in which all processors are idle and the queue is empty. We can compute the probability by setting p_{1}=0, p_{2}=3, p_{3}=0 as the initial state and checking the formula P_{=?}(♢^{≤t} p_{1}=3 ∧ p_{3}=0).
λ  Uniform  Layered  FSP exponential  prob.  

depth  time (s)  n  depth  time (s)  n  depth  time (s)  n  
40  609  0.9/1.2  2,434  533  0.9/1.1  2,130  512  2.8/1.3  2,046  4.22E04 
60  846  0.9/1.6  3,382  754  0.9/1.5  3,014  1,024  4.9/2.1  4,094  1.25E04 
80  1,077  0.9/2.1  4,306  971  0.9/1.9  3,882  1,024  4.9/2.0  4,094  5.27E05 
100  1,305  0.9/2.5  5,218  1,187  0.9/2.4  4,746  2,048  9.3/4.0  8,190  2.70E05 
Results for different λ are given in the table above for μ=1000, m=3, t=10. The precision used in the truncation computation was 10^{6}. The uniformization rate of the underlying CTMC is 1000+λ. With the increase of λ, the depth grows approximately linearly. Thus, the performance of the FSP configuration suffers from the high cost of repeated transient analysis, and, therefore, does not terminate within two hours. As observed by Munsky [MunskyK06] this problem can be alleviated by adding more than one layer at each step. We consider a variant in which we double the number of layers we add per step, thus computing an error estimate every 1,2,4,8,... layers. We call this configuration FSP exponential. In contrary to FSP, FSP exponential configuration works reasonable. It is however not competitive with the Uniform or Layered configuration in time and memory.
Protein Synthesis
We analyze an SPN model of protein synthesis [GossP98] as depicted in the figure below.
In biological cells, each protein is encoded by a certain gene. If the gene is active, the corresponding protein will be synthesized. Also, proteins may degenerate and thus disappear after a time. Activation and deactivation of genes, protein synthesis (in case of active gene) as well as protein degeneration are modeled by stochastic rates. In the model, the place p_{1} corresponds to an inactive gene encoding the protein, p_{2} corresponds to an active gene, and p_{3} gives the numbers of existing proteins. The transition t_{1} deactivates the gene with rate μ, while t_{2} activates it with rate λ. If the gene is active, t_{3} can produce new proteins with rate ν. Each individual protein degenerates with rate δ, which is modeled by the transition t_{4}. We consider the property that, within time t but later than 10 time units, a state is reached, in which 20 or more proteins exist and the gene is inactive: P_{=?} (♢^{[10,t]} p_{3} ≥ 20 ∧ inactive) where inactive is an atomic proposition representing inactive genes.
t  Uniform  Layered  FSP  prob.  

depth  time (s)  n  depth  time (s)  n  depth  time (s)  n  
300  2,330  0.9/2.0  4,659  2,047  0.9/1.7  4,093  34  1.0/0.0  67  2.07E02 
500  3,636  0.9/7.8  7,271  3,308  1.0/6.4  6,615  35  1.0/0.0  69  4.39E02 
1000  6,830  0.9/74.5  13,659  6,420  1.4/68.0  12,839  36  1.2/0.0  71  9.99E02 
2000  13,103  1.0/567.0  26,205  12,577  2.7/502.2  25,153  37  1.4/0.0  73  2.02E01 
The results for λ=1, μ=5, ν=1, δ=0.02 are presented in the table above. Here, for the computation of the truncation point we used a precision of 10^{6} In this case study, the sum of the outgoing rates of a state mainly depends on p_{3}⋅δ. Thus the model is rateunbounded. On newly explored states where p_{3} is higher, the uniformization rate could also be increased. Thus, in or initial paper [ZhangHHW08] only time bounds t≤45 can be handled. Since in the Uniform and Layered chain configurations only forward exit rates are considered, very large time bounds can now be handled. Remarkably, the depth grows very slowly with respect to time if FSP is used. Even though global rates are unbounded, this is of no consequence, since most of the rates lead back to states at lower depth. This also means that the probability of going out is very small. Both Uniform and Layered chain configuration do not exploit this. Thus the resulting truncation depth is significantly higher.
GridWorld Robot
We consider a grid world in which a robot moves from the lower left to the upper right corner sending signals to a station [Younes05a]. A janitor moves around and may block the robot for some time. In contrast to [Younes05a], the janitor can leave the N×N field of the robot, which leads to an infinite state space. We check the property "The probability that the robot reaches the upper right corner of the field within 100 time units while maintaining a probability of at least 0.5 of communicating periodically (every seven minutes) with a base station, is at least 0.9", which can be expressed via the CSL formula P_{≥0.9} ( ( P_{≥ 0.5} ♢^{≤ 7} communicate ) U^{≤100} upperright ). In the table below, we give results for different N. Using the FSP method is advantageous, as each layer of the model contains quite a large number of states, and FSP only needs to explore a fraction of the layers compared to the other methods. As seen from the "prob." column, for N=2,3 the property holds, while, for N=4, it does not. The reason for the decreasing probability is that the distance the robot has to travel increases with n. Thus the probability decreases that the robot will complete its travel in time. In this case study, an implicit representation of the transitions of the model is used to avoid running out of memory. During the analysis, each time we visit a state, we compute its outgoing transitions on the fly. Afterwards, these transitions are removed and the next state is considered. The tradeoff of this representation is the increasing runtime.
N  Uniform  Layered  FSP  prob.  

depth  time (s)  n  depth  time (s)  n  depth  time (s)  n  
2  912  35/16K  9,960K  576  14/6K  3,969K  31  59/12  11K  9.99E01 
3  912  58/35K  16,563K  576  26/13K  6,591K  31  91/22  17K  9.01E01 
4  912  79/51K  23,137K  576  34/19K  9,194K  32  126/32  24K  8.95E01 
Tandem Queueing Network
This model [HermannsMS99] consists of two interconnected queues with capacity c. We consider the probability that the first queue becomes full before time 0.23. Larger time bounds are left out, since then this probability is one. The performance results forINFAMY
using configuration Layered are better, while for
large time bound (t≥ 1) the whole model will be explored thus
PRISM
will perform better.
c  PRISM 
Layered  prob.  

depth  time  n  depth  time  n  
511  1,535  3.7/49.7  523,776  632  6.8/7.5  235,339  3.13E02 
1023  3,071  13.7/380.3  2,096,128  1,167  3.6/49.6  714,306  4.24E03 
2047  6,143  69.3/3,068.3  8,386,560  2,198  10.0/297.8  2,449,798  9.87E05 
4095  12,287  560.9/31,386.5  33,550,336  4,209  27.4/2,889.8  8,899,113  7.06E08 
Workstation cluster
While the previously discussed case studies lead to infinite CTMCs, we
now assess our method on finitestate models. To compare
against a model checker which does not employ truncation, we use
PRISM
[HintonKNP06]
in version 3.2, which was latest when handling this case study.
We consider the dependability of a faulttolerant workstation cluster [HaverkortHK00]. The figure below depicts a dependable cluster of workstations. The cluster consists of two subclusters, which, in turn, contain N workstations connected via a central switch. The two switches are connected via a backbone. Each component of the system can break down, and is then fixed by a single repair unit responsible for the entire system. Hereby, the quality of service (QoS) constraint
Minimum requires at least k (k < N) workstations to be operational where k=⌊¾N⌋. Workstations have to be connected via switches. If in each subcluster the number of operational workstations is smaller than k the backbone is required to be operational to provide the required service. We consider two properties:
 P_{=?} (♢^{[0,1]} ¬Minimum): the probability that the QoS drops below minimum quality within one time unit.

the expected number of repairs by time point one. The
corresponding property on the
PRISM
website is R=?[C<=T].
For both properties, we compare PRISM
with INFAMY
. The results are given in the table
below. Because the resulting probabilities are very small in some
cases, we use a precision of 10^{12} here, for the
computation of the truncation point. Results for INFAMY
are given for the Layered chain and FSP configurations
respectively. The Uniform chain configuration is omitted, as it is
always dominated by the Layered chain
configuration. PRISM
implements three different
engines: a sparsematrix and two symbolic engines. We used the
sparsematrix engine as it was the fastest one.
N  PRISM 
Layered  FSP  prob./exp.  

dep  tm (s)  n  dep  tm (s)  n  dep  tm (s)  n  
512  1029  12/197/952  9466K  105  2/5/5  193K  20  2/0/0  6K  5.96E08/0.72 
1024  2053  48/1132/  37806K  109  2/5/5  208K  26  3/0/0  11K  6.01E08/1.08 
2048        116  2/6/6  236K  36  6/1/1  22K  .07E08/1.38 
4096        129  3/7/8  293K  53  19/1/1  48K  6.11E08/1.56 
In the table above, the time columns "tm (s)" have the
format t_{1}/t_{2}/t_{3} where the
first number t_{1} denotes the time needed for model
construction, t_{2} for the time to check property 1
and t_{3} that for property 2. While the number of
states and transitions for PRISM
increases dramatically
with parameter N, INFAMY
scales much better in
both configurations. The reason is apparent from the column
displaying the depth: the depth of the full model is approximately
linear in N, while the depth needed is sublinear
in N. For N≥2048 and N≥1024 respectively,
PRISM
cannot model check these properties as it runs out
of memory and crashes; this is denoted by "". As N
increases, the truncation depth grows only slowly
in INFAMY
and hence, only a small fraction of the state
space needs to be explored in the truncated construction. Although the
FSP configuration is not very effective in terms of the total time,
thereby spending the largest part of the running time in the first
phase, it shows a lot of potential in terms of depth and number of
states.
In the table below, we give additional performance measures for a
model of N=512 workstations for property 1 for larger
time bounds. Results are given for PRISM
(sparse engine),
FSP and FSP exponential respectively. The state space explored by
PRISM
has depth 1029 and includes 9.4 million states. Up
to t=20, INFAMY
with FSP is faster than
PRISM
. However, for larger time bounds, the model
construction time dominates, as for each layer exploration the error
estimate is recomputed. The FSP variant with exponential layer
explorations is suitable for this case, and is consistently the
fastest method for t≤ 50, as shown in the last column of the
table.
t  PRISM 
FSP  FSP exponential  prob.  

time (s)  depth  time (s)  n  depth  time (s)  n  
10.0  11.9/359.5  52  47.5/3.0  46K  64  6.8/4.7  71K  3.79E06 
20.0  11.7/593.8  80  318.1/13.5  111K  128  44.4/35.6  289K  1.01E05 
30.0  11.7/802.2  104  1,016.9/32.5  190K  128  62.5/50.2  289K  1.68E05 
50.0  11.7/1171.8  147  4,660.4/103.7  382K  256  404.9/323.0  1,167K  3.04E05 