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.