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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
We’re sorry, something doesn't seem to be working properly.
Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.
Keywords
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
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)
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)
Buchholz, P.: Exact and ordinary lumpability in finite Markov chains. J. of Applied Probability 31, 59–75 (1994)
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)
Cloth, L., Haverkort, B.R., Jongerden, M.: Computing battery lifetime distributions. In: DSN, pp. 780–789. IEEE Computer Society Press, Los Alamitos (2007)
Davis, M.H.A.: Markov Models and Optimization. Chapman and Hall, Boca Raton (1993)
Derisavi, S., Hermanns, H., Sanders, W.H.: Optimal state-space lumping in Markov chains. Inf. Processing Letters 87(6), 309–315 (2003)
Dovier, A., Piazza, C., Policriti, A.: An efficient algorithm for computing bisimulation equivalence. Theor. Comput. Sci. 311(1-3), 221–256 (2004)
Everdij, M., Blom, H.: Piecewise deterministic Markov processes represented by dynamically coloured Petri nets. Stochastics 77(1), 1–29 (2005)
Fernandez, J.C.: An implementation of an efficient algorithm for bisimulation equivalence. Science of Computer Programming 13, 219–236 (1989)
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)
Haghverdi, E., Tabuada, P., Pappas, G.J.: Bisimulation relations for dynamical, control, and hybrid systems. Theor. Comput. Sci. 342(2-3), 229–261 (2005)
Han, T., Katoen, J.-P., Mereacre, A.: Compositional Modeling and Minimization of Time-Inhomogeneous Markov Chains. Technical report AIB200721, RWTH Aachen, Germany (2007)
Hermanns, H.: Interactive Markov Chains. LNCS, vol. 2428. Springer, Heidelberg (2002)
Hermanns, H., Herzog, U., Katoen, J.-P.: Process algebra for performance evaluation. Theor. Comput. Sci. 274(1-2), 43–87 (2002)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Kailath, T.: Linear Systems. Prentice-Hall, Englewood Cliffs (1980)
Katoen, J.-P.: Stochastic model checking. In: Stochastic Hybrid Systems, pp. 79–106. CRC Press, Boca Raton (2006)
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)
Milner, R.J.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Paige, R., Tarjan, R.: Three partition refinement algorithms. SIAM J. of Computing 16(6), 973–989 (1987)
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)
Strubbe, S.N., Julius, A.A., van der Schaft, A.J.: Communicating piecewise deterministic Markov processes. In: ADHS, pp. 349–354 (2003)
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)
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)
Author information
Authors and Affiliations
Editor information
Rights 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)