Bounds based on lumpable matrices for partially ordered state space

We consider the strong stochastic ("st") ordering on Markov chains whose states are naturally endowed with a partial order and we present an algorithmic derivation of lumpable upper bounding matrix.The comparison of Markov chains relies on the monotonicity property even if it is only sufficient. When the model is not monotone, we must build a monotone upper bound. Quite often the natural partial order of the model makes the problem monotone with this order. However, if we use a total order consistent with the partial one the model is often not monotone anymore for the total order. Furthermore, the monotonicity property for total order adds a lot of constraints which are irrelevant and make the bound less accurate.Here we assume that the model is monotone for the natural partial order and we must build a matrix which is larger in the strong stochastic sense and easier to solve. We build a lumpable bound and we store the lumped version to be analyzed.Lumpable upper bounding matrices may also be useful when they are associated to a total order. We can derive a bound of the Markov chain with a two phase algorithm: first we derive a lumpable upper bound from the specifications, we store the lumped version and we make this lumped matrix monotone in a second phase.