Hierarchical Markovian models: symmetries and reduction

Hierarchical Markovian models are a useful paradigm for the specification and quantitative analysis of models arising from complex systems. Although techniques for a very efficient analysis of large scale hierarchical Markovian models have been developed recently, the size of the Markov chain underlying a complex hierarchical model often prohibits an analysis on contemporary computer equipment. However, many realistic models contain a lot of symmetric and identical parts, allowing the construction of a reduced Markov chain yielding exact results for the complete model. Of course, to make use of symmetries in a fairly complex model, a technique is needed that generates automatically a reduced Markov chain from the specification of the model. Such an approach can be integrated in an appropriate modelling tool environment for the analysis of hierarchical models and often yields a dramatic reduction in the state space size allowing the analysis of models that are far too large to be solved by standard means.