Statistical Verification of Probabilistic Properties with Unbounded Until - Formal Methods: Foundations and Applications - page 155

As with Y T , Z k does not have the same expectation of X , although we do have
lim k→∞ Z k = X . The expected value for Z k is estimated for a series of increasing
values for k until some convergence criterion is met. Lassaigne and Peyronnet [18]
relate the choice of k to the subdominant eigenvalue, but as with the other
theoretical results mentioned earlier that involve the subdominant eigenvalue,
this result does not help to choose k in practice. Ensuring a certain accuracy
becomes hard because each successive iteration with a different value for k is
subject to error, and different ad-hoc termination criteria are proposed by the
various authors. In the solution methods presented in this paper, we avoid this
iterative estimation approach by always setting up experiments that preserve
the expected value of the quantity of interest.
Rabih et al. [7] present a very different simulation-based approach to verifying
unbounded until properties. They develop an algorithm based on perfect simula-
tion. The approach is interesting, but impractical unless the model is monotone.
The authors do not discuss how to determine monotonicity for a model, or
whether the widely-used PRISM benchmarks satisfy this property, so it is hard
to assess the general applicability of their method.
The termination-probability approach has been used for rare-event simula-
tion (see, e.g., [19]). Improvements to the basic algorithm from the simulation
community would be valuable for model checking as well.

5 Empirical Evaluation

We use two continuous-time Markov-chain models as the basis for our empirical
evaluation, with rather different characteristics. Note that model checking of un-
bounded until for continuous-time Markov-chains reduces to model checking for
the embedded discrete-time Markov chain [1]. Thus, a continuous-time Markov
chain presents no additional challenge for the algorithms described in Sect. 3.

5.1 Modified Polling System

The first model is a variation of an n -station symmetric polling system, described
by Ibe and Trivedi [16]. In the original polling-system model, each station has a
single-message buffer and the stations are attended to by a single server in cyclic
order. When attending to a station, the server checks for a message in the buffer
of the station by polling the station, and goes on to serve the station if there is a
message. The polling and service times are exponentially distributed with rates
γ = 200 and μ = 1, respectively. Furthermore, each station has an inter-arrival
time for messages that is exponentially distributed with rate λ =1 /n .
Here, we consider a modified version of the polling-system model, where
polling stations can fail and stop accepting messages. The failure rate of a station
is κ = λ/ 3. After a station has failed, it can never be served again. This way,
infinite sample trajectories become a possibility for the property we consider.
We verify the following property: the probability is at least 0.4 that station 1
is served before station 2. Let s ∈{ 1 ,...,n } be the station currently attended