Skip to main content
SpringerLink
Log in

Compositional Modeling and Minimization of Time-Inhomogeneous Markov Chains

  • Conference paper
Book cover Hybrid Systems: Computation and Control (HSCC 2008)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4981))

Included in the following conference series:

Abstract

This paper presents a compositional framework for the modeling of interactive continuous-time Markov chains with time-dependent rates, a subclass of communicating piecewise deterministic Markov processes. A poly-time algorithm is presented for computing the coarsest quotient under strong bisimulation for rate functions that are either piecewise uniform or (piecewise) polynomial. Strong as well as weak bisimulation are shown to be congruence relations for the compositional framework, thus allowing component-wise minimization. In addition, a new characterization of transient probabilities in time-inhomogeneous Markov chains with piecewise uniform rates is provided.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Grosu, R., Hur, Y., Kumar, V., Lee, I.: Modular specification of hybrid systems in CHARON. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 6–19. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  2. Alur, R., Grosu, R., Sokolsky, O., Lee, I.: Compositional modeling and refinement for hierarchical hybrid systems. J. Log. Algebr. Program. 68(1-2), 105–128 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  3. Buchholz, P.: Exact and ordinary lumpability in finite Markov chains. J. of Applied Probability 31, 59–75 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  4. Bujorianu, M.L., Lygeros, J., Bujorianu, M.C.: Bisimulation for general stochastic hybrid systems. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 198–214. Springer, Heidelberg (2005)

    Google Scholar 

  5. Cloth, L., Haverkort, B.R., Jongerden, M.: Computing battery lifetime distributions. In: DSN, pp. 780–789. IEEE Computer Society Press, Los Alamitos (2007)

    Google Scholar 

  6. Davis, M.H.A.: Markov Models and Optimization. Chapman and Hall, Boca Raton (1993)

    MATH  Google Scholar 

  7. Derisavi, S., Hermanns, H., Sanders, W.H.: Optimal state-space lumping in Markov chains. Inf. Processing Letters 87(6), 309–315 (2003)

    Article  MathSciNet  Google Scholar 

  8. Dovier, A., Piazza, C., Policriti, A.: An efficient algorithm for computing bisimulation equivalence. Theor. Comput. Sci. 311(1-3), 221–256 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  9. Everdij, M., Blom, H.: Piecewise deterministic Markov processes represented by dynamically coloured Petri nets. Stochastics 77(1), 1–29 (2005)

    MATH  MathSciNet  Google Scholar 

  10. Fernandez, J.C.: An implementation of an efficient algorithm for bisimulation equivalence. Science of Computer Programming 13, 219–236 (1989)

    Article  Google Scholar 

  11. Fisler, K., Vardi, M.Y.: Bisimulation minimization in an automata-theoretic verification framework. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 115–132. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  12. Haghverdi, E., Tabuada, P., Pappas, G.J.: Bisimulation relations for dynamical, control, and hybrid systems. Theor. Comput. Sci. 342(2-3), 229–261 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  13. Han, T., Katoen, J.-P., Mereacre, A.: Compositional Modeling and Minimization of Time-Inhomogeneous Markov Chains. Technical report AIB200721, RWTH Aachen, Germany (2007)

    Google Scholar 

  14. Hermanns, H.: Interactive Markov Chains. LNCS, vol. 2428. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  15. Hermanns, H., Herzog, U., Katoen, J.-P.: Process algebra for performance evaluation. Theor. Comput. Sci. 274(1-2), 43–87 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  16. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  17. Kailath, T.: Linear Systems. Prentice-Hall, Englewood Cliffs (1980)

    MATH  Google Scholar 

  18. Katoen, J.-P.: Stochastic model checking. In: Stochastic Hybrid Systems, pp. 79–106. CRC Press, Boca Raton (2006)

    Google Scholar 

  19. Katoen, J.-P., Kemna, T., Zapreev, I.S., Jansen, D.N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 76–92. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  20. Milner, R.J.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  21. Paige, R., Tarjan, R.: Three partition refinement algorithms. SIAM J. of Computing 16(6), 973–989 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  22. Rindos, A., Woolet, S., Viniotis, I., Trivedi, K.S.: Exact methods for the transient analysis of non-homogeneous continuous-time Markov chains. In: Numerical Solution of Markov Chains (NSMC), pp. 121–134. Kluwer, Dordrecht (1995)

    Google Scholar 

  23. Strubbe, S.N., Julius, A.A., van der Schaft, A.J.: Communicating piecewise deterministic Markov processes. In: ADHS, pp. 349–354 (2003)

    Google Scholar 

  24. Strubbe, S.N., van der Schaft, A.J.: Compositional modelling of stochastic hybrid systems. In: Stochastic Hybrid Systems, pp. 47–77. CRC Press, Boca Raton (2006)

    Google Scholar 

  25. Strubbe, S.N., van der Schaft, A.J.: Bisimulation for communicating piecewise deterministic Markov processes (CPDPs). In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 623–639. Springer, Heidelberg (2005)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Software Modeling and Verification Group, RWTH Aachen University, Germany

    Tingting Han, Joost-Pieter Katoen & Alexandru Mereacre

  2. Formal Methods and Tools Group, University of Twente, The Netherlands

    Tingting Han & Joost-Pieter Katoen

  3. Dept. of Information and Communication Technology, University of Trento, Italy

    Alexandru Mereacre

Authors
  1. Tingting Han
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Joost-Pieter Katoen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alexandru Mereacre
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Magnus Egerstedt Bud Mishra

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Han, T., Katoen, JP., Mereacre, A. (2008). Compositional Modeling and Minimization of Time-Inhomogeneous Markov Chains. In: Egerstedt, M., Mishra, B. (eds) Hybrid Systems: Computation and Control. HSCC 2008. Lecture Notes in Computer Science, vol 4981. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78929-1_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-78929-1_18

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-78928-4

  • Online ISBN: 978-3-540-78929-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation