Reachable State Space Generation for Structured Models which Use Functional Transitions

This paper presents a new approach to obtain the reachable state space (RSS) of a structured model which uses functional transitions. We use multi-valued decision diagrams (MDD) to store sets of reachable spaces and stochastic automata networks (SAN) formalism to describe structured models. We focus our contribution in the proposal of a method to generate a compact MDD description taking advantage of the modular structure of SAN formalism, which also allows to represent the transition rate matrix of a continuous-time Markov chain by means of a sum of generalized Kronecker products. The method is tested on some models and the conclusion presents future work.