Advertisement

An Experimental Evaluation of Probabilistic Simulation

  • Jonathan Bogdoll
  • Holger Hermanns
  • Lijun Zhang
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5048)

Abstract

Probabilistic model checking has emerged as a versatile system verification approach, but is frequently facing state-space explosion problems. One promising attack to this is to construct an abstract model which simulates the original model, and to perform model checking on that abstract model. Recently, efficient algorithms for deciding simulation of probabilistic models have been proposed. They reduce the theoretical complexity bounds drastically by exploiting parametric maximum flow algorithms. In this paper, we report on experimental comparisons of these algorithms, together with various interesting optimizations. The evaluation is carried out on both standard PRISM example cases as well as randomly generated models. The results show interesting time-space tradeoffs, with the parametric maximum flow algorithms being superior for large, dense models.

Keywords

Decision Algorithm Leader Election Simulation Relation Probabilistic Simulation Parametric Maximum 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269–276. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  2. 2.
    Baier, C., Engelen, B., Majster-Cederbaum, M.E.: Deciding bisimilarity and similarity for probabilistic processes. J. Comput. Syst. Sci. 60(1), 187–231 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Software Eng. 29(6), 524–541 (2003)CrossRefzbMATHGoogle Scholar
  4. 4.
    Baier, C., Katoen, J.-P., Hermanns, H., Haverkort, B.: Simulation for continuous-time Markov chains. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 338–354. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  5. 5.
    Baier, C., Katoen, J.-P., Hermanns, H., Wolf, V.: Comparative branching-time semantics for Markov chains. Inf. Comput. 200(2), 149–214 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Bianco, A., de Alfaro, L.: Model Checking of Probabilistic and Nondeterministic Systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, Springer, Heidelberg (1995)CrossRefGoogle Scholar
  7. 7.
    Bohnenkamp, H.C., van der Stok, P., Hermanns, H., Vaandrager, F.W.: Cost-optimization of the ipv4 zeroconf protocol. In: DSN, pp. 531–540 (2003)Google Scholar
  8. 8.
    Gallo, G., Grigoriadis, M.D., Tarjan, R.E.: A fast parametric maximum flow algorithm and applications. SIAM J. Comput. 18(1), 30–55 (1989)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Goldberg, A.V., Tarjan, R.E.: A new approach to the maximum-flow problem. J. ACM 35(4), 921–940 (1988)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Groß, C., Hermanns, H., Pulungan, R.: Does clock precision influence ZigBee’s energy consumptions? In: Tovar, E., Tsigas, P., Fouchal, H. (eds.) OPODIS 2007. LNCS, vol. 4878, pp. 174–188. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  11. 11.
    Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Asp. Comput. 6(5), 512–535 (1994)CrossRefzbMATHGoogle Scholar
  12. 12.
    Hinton, A., Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: A Tool for Automatic Verification of Probabilistic Systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  13. 13.
    Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266–277 (1991)Google Scholar
  14. 14.
    Katoen, J.-P., Kemna, T., Zapreev, I., Jansen, D.N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 87–101. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  15. 15.
    Katoen, J.-P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: QEST, pp. 243–244 (2005)Google Scholar
  16. 16.
    Mangold, S., Zhong, Z., Hiertz, G.R., Walke, B.: Ieee 802.11e/802.11k wireless lan: spectrum awareness for distributed resource sharing. Wireless Communications and Mobile Computing 4(8), 881–902 (2004)CrossRefGoogle Scholar
  17. 17.
    Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nord. J. Comput. 2(2), 250–273 (1995)MathSciNetzbMATHGoogle Scholar
  18. 18.
    Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press, Princeton (1994)zbMATHGoogle Scholar
  19. 19.
    Tabakov, D., Vardi, M.Y.: Experimental evaluation of classical automata constructions. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 396–411. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  20. 20.
    Zhang, L., Hermanns, H.: Deciding simulations on probabilistic automata. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 207–222. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  21. 21.
    Zhang, L., Hermanns, H., Eisenbrand, F., Jansen, D.N.: Flow faster: Efficient decision algorithms for probabilistic simulations. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 155–169. Springer, Heidelberg (2007)CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2008

Authors and Affiliations

  • Jonathan Bogdoll
    • 1
  • Holger Hermanns
    • 1
  • Lijun Zhang
    • 1
  1. 1.Department of Computer ScienceSaarland UniversitySaarbrückenGermany

Personalised recommendations