Signature-based Symbolic Algorithm for Optimal Markov Chain Lumping

Many approaches to tackle the state-space explosion problem of Markov chains are based on the notion of lumpability (a.k.a. probabilistic bisimulation), 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 a new signature-based algorithm for computing the optimal (i.e., smallest possible) quotient Markov chain, prove its correctness, and implement it symbolically for Markov chains represented as Multi-Terminal BDDs (MTBDDs). The algorithm is very time-efficient because we translate the core operation of the algorithm, i.e., the computation of the signatures, into symbolic operations. Our experiments on various configurations of three example models with different levels of lump ability show that the algorithm (1) handles significantly larger state spaces than an explicit algorithm, (2) outperforms a very efficient explicit algorithm for significantly lump able Markov chains while it is not prohibitively slower in the worst case, and (3) outperforms our previous optimal symbolic algorithm [10] in terms of running time although it has higher space requirement for most of the configurations.