Abstract
Many approaches to tackle the state explosion problem of Markov chains are based on the notion of lumpability, which allows computation of measures using the quotient Markov chain, which, in some cases, has much smaller state space than the original one. We present, for the first time, a symbolic algorithm and its implementation for the lumping of Markov chains that are represented using Multi-Terminal Binary Decision Diagrams. The algorithm is optimal, i.e., generates the smallest possible quotient Markov chain. Our experiments on various configurations of two example models show that the algorithm (1) handles significantly larger state spaces than an explicit algorithm, (2) is in the best case, faster than an efficient explicit algorithm while not prohibitively slower in the worst case, and (3) generates quotient Markov chains that are several orders of magnitude smaller than ones generated by a model-dependent symbolic lumping algorithm.
Chapter PDF
Similar content being viewed by others
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
Böde, E., et al.: Compositional performability evaluation for STATEMATE. In: Proc. of QEST, USA (Sep. 2006)
Bouali, A., de Simone, R.: Symbolic bisimulation minimisation. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 96–108. Springer, Heidelberg (1993)
Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Comp. 35(8), 677–691 (1986)
Buchholz, P.: Exact and ordinary lumpability in finite Markov chains. Journal of Applied Probability 31, 59–74 (1994)
Buchholz, P.: Efficient computation of equivalent and reduced representations for stochastic automata. Int. Journal of Comp. Sys. Sci. & Eng. 15(2), 93–103 (2000)
Ciardo, G., Miner, A.S.: A data structure for the efficient Kronecker solution of GSPNs. In: Proc. of PNPM, pp. 22–31 (1999)
Clarke, E., et al.: Multiterminal binary decision diagrams: An efficient data structure for matrix representation. Formal Methods in System Design 10(2-3), 149–169 (1997)
Derisavi, S.: Solution of Large Markov Models Using Lumping Techniques and Symbolic Data Structures. PhD thesis, U. of Illinois at Urbana-Champaign (2005)
Derisavi, S., Hermanns, H., Sanders, W.H.: Optimal state-space lumping in Markov chains. Information Processing Letters 87(6), 309–315 (2003)
Derisavi, S., Kemper, P., Sanders, W.H.: Symbolic state-space exploration and numerical analysis of state-sharing composed models. Linear Algebra and Its Applications 386, 137–166 (2004)
Derisavi, S., Kemper, P., Sanders, W.H.: Lumping matrix diagram representations of markovian models. In: Proc. of DSN, Japan, pp. 742–751 (2005)
Hermanns, H.: Interactive Markov Chains. LNCS, vol. 2428. Springer, Heidelberg (2002)
Hermanns, H., Meyer-Kayser, J., Siegle, M.: Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains. In: Proc. of 3rd Meeting on Numerical Solution of Markov Chains (NSMC), pp. 188–207 (1999)
Hermanns, H., Siegle, M.: Bisimulation Algorithms for Stochastic Process Algebras and Their BDD-Based Implementation. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 244–264. Springer, Heidelberg (1999)
Hinton, A., et al.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)
Howard, R.A.: Dynamic Probabilistic Systems, Volume II: Semi-Markov and Decision Processes. Wiley, New York (1971)
Kemeney, J.G., Snell, J.L.: Finite Markov Chains. D. Van Nostrand Company, New York (1960)
Kwiatkowska, M., Norman, G., Parker, D.: Symmetry reduction for probabilistic model checking. In: Huang, D.-S., Li, K., Irwin, G.W. (eds.) ICIC 2006. LNCS (LNAI), vol. 4114, pp. 234–248. Springer, Heidelberg (2006)
Sanders, W.H., Malhis, L.M.: Dependability evaluation using composed SAN-based reward models. J. of Para. and Dist. Comp. 15(3), 238–254 (1992)
Sanders, W.H., Meyer, J.F.: Reduced base model construction methods for stochastic activity networks. IEEE J. on Selected Areas in Comm. 9(1), 25–36 (1991)
Somenzi, F.: CUDD: Colorado University decision diagram package. Public software, Colorado Univeristy, Boulder, http://vlsi.colorado.edu/~fabio/
Hermanns, H., et al.: Sigref – A Symbolic Bisimulation Tool Box. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 477–492. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Derisavi, S. (2007). A Symbolic Algorithm for Optimal Markov Chain Lumping. In: Grumberg, O., Huth, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2007. Lecture Notes in Computer Science, vol 4424. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71209-1_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-71209-1_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71208-4
Online ISBN: 978-3-540-71209-1
eBook Packages: Computer ScienceComputer Science (R0)