On the Detection of Symmetries in Compositional Markov Models

A model-based evaluation of a system’s design often considers to what degree components need to be available multiple times in order to reach a desired level of availability, reliability or dependability. Multiple components of the same kind then lead to models with regular structures and symmetries. In stochastic models, especially Markovian models, such regularities have been used to establish lumpability results. In this paper, we propose a procedure to detect symmetries in a Markovian model that is built in a compositional manner by sharing state variables. The symmetries give insight into a model and help to achieve a significant state space reduction, which alleviates the effects of the infamous state space explosion problem. The results extend existing work of Obal, McQuinn, and Sanders; in particular, we focus on variables in functional transition rates that commute in order to take additional symmetries into account. The overall approach contributes to Mobius, a multi-paradigm, multi-solution framework for the model-based dependability and performance assessment of systems.