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

tandem queuing network, using the same algorithms as before. Again, the results
for sampling-based approaches are averages over 20 trials.
For this model, the sampling-based algorithm that uses termination probabil-
ity comes out on top. The reason is that reachability analysis is much more ex-
pensive for this model. The difference between Hoeffding and SPRT gets smaller
for larger state spaces, as the time needed to perform reachability analysis starts
to dominate the difference in sample size (446 for SPRT; 105,967 for Hoeffding).
6 Discussion
We have presented two sampling-based algorithms for probabilistic model check-
ing of time-unbounded properties. Both solution methods are based on unbiased
estimators. This avoids the convergence issues that haunt existing sampling-
based algorithms, which all use biased estimators. The first method, especially,
is valuable as it provides correctness guarantees that are independent of any
model parameters. The second method has the same weakness as popular iter-
ative numerical solution methods, in that accuracy cannot be guaranteed fully
without knowledge of the subdominant eigenvalue. Still, it allows us to analyze
models far beyond the reach of methods that require model construction (as is
the case for the first method, as well as numerical methods). Future work could
focus on extending the theoretical results of this paper. In particular, conditions
under which X T has finite variance should be established for a more general
class of systems. Techniques from the simulation community should be incorpo-
rated to reduce the variance of X T , and the empirical coverage probability for
sequential estimation should be established.
Acknowledgments. Edmund M. Clarke and Paolo Zuliani were supported in
part by the GSRC under contract no. 1041377, National Science Foundation
under award no. CNS0926181, no. CCF0541245, and no. CNS0931985, Semicon-
ductor Research Corporation under contract no. 2005TJ1366, General Motors
under contract no. GMCMUCRLNV301, Air Force under contract no. 18727S3,
and the Oce of Naval Research under award no. N000141010188.
References
1. Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algo-
rithms for continuous-time Markov chains. IEEE Transactions on Software Engi-
neering 29(6), 524-541 (2003)
2. Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge
(2008)
3. Basu, S., Ghosh, A.P., He, R.: Approximate model checking of PCTL involving
unbounded path properties. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009.
LNCS, vol. 5885, pp. 326-346. Springer, Heidelberg (2009)