During the project the current model construction will be analysed in regard to performance(i.e. reachability of multiple initial states, scalability and comprehensiveness(adding support for other types of models, i.e. PTAs). Depending on the analysis, it is decided which changes in the current approach enhance the functionality/ performance/ scalability and together with the supervisor a feature list can be defined. Then the implementation of the features is conducted and additionally efficient transformation to a sparse model and full import/export of the explicit model is implemented.