Advertisement

Solving Large Markov Models Described with Standard Programming Language

  • P. Pecka
  • M. P. Nowak
  • A. Rataj
  • S. Nowak
Conference paper
Part of the Communications in Computer and Information Science book series (CCIS, volume 935)

Abstract

Continuous time Markov chains (CTMC) are one of the formalisms for building models. This paper discusses OLYMP2 - a system for solving big CTMC models (exceeding \(10^9\) states), described with a standard programming language - Java. OLYMP2 is primarily aimed at modelling of computer networks, so its formalism comes from networking concepts, like queueing systems. Using Java as a model description allows for greater flexibility in comparison to model-checker specific languages that often do not employ complete features of an object-oriented programming. Using Java also makes the parsing of models relatively fast, due to optimised Java run-time environment. Introducing dedicated compression of transition matrices allows for keeping memory usage at reasonable level even for large models.

Keywords

Markov chains Model checker Performance evaluation 

References

  1. 1.
    Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008). ISBN-13:978-0-262-02649-9Google Scholar
  2. 2.
    Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-30080-9_7CrossRefGoogle Scholar
  3. 3.
    Czachórski, T., Grochla, K., Józefiok, A., Nycz, T.: Simulation, markov chain and diffusion approximation models–a case study. In: Computer Science & Information Technologies (CSIT2011) (2011)Google Scholar
  4. 4.
    Erlang, A.: Solution of some problems in the theory of probabilities of significance in automatic telephone exchanges, post office. Electr. Eng. J. 10, 189–197 (1918)Google Scholar
  5. 5.
    Fourneau, J.M., Mahjoub, Y.A.E., Quessette, F., Vekris, D.: XBorne 2016: a brief introduction. In: Czachórski, T., Gelenbe, E., Grochla, K., Lent, R. (eds.) ISCIS 2016. CCIS, vol. 659, pp. 134–141. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-47217-1_15CrossRefGoogle Scholar
  6. 6.
    Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Form. Asp. Comput. 6(5), 512–535 (1994)CrossRefGoogle Scholar
  7. 7.
    Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual, 4th edn. Addison-Wesley, Boston (2008). OCLC:254420839Google Scholar
  8. 8.
    Kirschnick, M.: The performance evaluation and prediction system for queueing networks-PEPSY-QNS. Technical Report TR-I4-18-94, Department of Computer Science 4, Universität Erlangen-Nürnberg, Germany (1994)Google Scholar
  9. 9.
    Krieger, U.R., Muller-Clostermann, B., Sczittnick, M.: Modeling and analysis of communication systems based on computational methods for markov chains. IEEE J. Sel. Areas Commun. 8(9), 1630–1648 (1990)CrossRefGoogle Scholar
  10. 10.
    Nowak, M., Pecka, P.: Reducing the number of states for markovian model of optical slotted ring network. In: Balandin, S., Dunaytsev, R., Koucheryavy, Y. (eds.) NEW2AN/ruSMART -2010. LNCS, vol. 6294, pp. 231–241. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14891-0_21CrossRefGoogle Scholar
  11. 11.
    Parzen, E.: Stochastic Processes. Classics in applied mathematics. Society for Industrial and Applied Mathematics (1999)Google Scholar
  12. 12.
    Pecka, P.: Obiektowo zorientowany wielowątkowy system do modelowania stanów nieustalonych w sieciach komputerowych za pomocą łanńcuchów Markowa (in Polish). PhD thesis, IITiS PAN, Gliwice (2002)Google Scholar
  13. 13.
    Pecka, P., Deorowicz, S., Nowak, M.: Efficient representation of transition matrix in the markov process modeling of computer networks. In: Kacprzyk, J., Czachórski, T., Kozielski, S., Stańczyk, U. (eds.) Man-Machine Interactions 2, vol. 103, pp. 457–464. Springer, Berlin (2011)Google Scholar
  14. 14.
    Rataj, A.: More flexible models using a new version of the translator of Java sources to timed automatons J2tadd. Theor. Appl. Inform. 21(2), 107–114 (2009)Google Scholar
  15. 15.
    Rataj, A., Woźna, B., Zbrzezny, A.: A translator of java programs to TADDs. Fundam. Inf. 93(1–3), 305–324 (2009)MathSciNetzbMATHGoogle Scholar
  16. 16.
    Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press, Princeton (1994)Google Scholar
  17. 17.
    Visser, W., Pasareanu, C.S., Khurshid, S.: Test input generation with java PathFinder. ACM SIGSOFT Softw. Eng. Notes 29(4), 97 (2004)CrossRefGoogle Scholar
  18. 18.
    Zbrzezny, A., Woźna, B.: Towards verification of Java programs in VerICS. Fundam. Inform. 85(1–4), 533–548 (2008)zbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Institute of Theoretical and Applied InformaticsGliwicePoland

Personalised recommendations