Advertisement

Tulip: Model Checking Probabilistic Systems Using Expectation Maximisation Algorithm

  • Rastislav Lenhardt
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8054)

Abstract

We describe a novel tool for model checking ω-regular specifications on interval Markov chains, recursive interval Markov chains and interval stochastic context-free grammars. The core of the tool is an iterative expectation maximisation procedure to compute values for the unknown probabilities in a parametrised system, which maximises the probability of satisfying the specification. The tool supports specifications given as LTL formulas or unambiguous Büchi automata.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Baum, L.E., Petrie, T., Soules, G., Weiss, N.: A maximization technique occurring in the statistical analysis of probabilistic functions of markov chains. The Annals of Mathematical Statistics 41(1), 164–171 (1970)MathSciNetzbMATHCrossRefGoogle Scholar
  2. 2.
    Benedikt, M., Lenhardt, R., Worrell, J.: LTL model checking of interval markov chains. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 32–46. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  3. 3.
    D’Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reachability analysis of probabilistic systems by successive refinements. In: de Luca, L., Gilmore, S. (eds.) PAPM-PROBMIV 2001. LNCS, vol. 2165, pp. 39–56. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  4. 4.
    Etessami, K., Yannakakis, M.: Recursive markov chains, stochastic grammars, and monotone systems of nonlinear equations. In: Diekert, V., Durand, B. (eds.) STACS 2005. LNCS, vol. 3404, pp. 340–352. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  5. 5.
    Etessami, K., Yannakakis, M.: Recursive markov decision processes and recursive stochastic games. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 891–903. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. 6.
    Fehnker, A., Gao, P.: Formal verification and simulation for performance analysis for probabilistic broadcast protocols. In: Kunz, T., Ravi, S.S. (eds.) ADHOC-NOW 2006. LNCS, vol. 4104, pp. 128–141. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  7. 7.
    Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS (1991)Google Scholar
  8. 8.
    Wojtczak, D., Etessami, K.: PReMo: An analyzer for probabilistic recursive models. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 66–71. Springer, Heidelberg (2007)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Rastislav Lenhardt
    • 1
  1. 1.Department of Computer ScienceUniversity of OxfordUnited Kingdom

Personalised recommendations