Applying symbolic techniques to the representation of non-markovian models with continuous ph distributions

Abstract

Among the proposed techniques for the analysis of non-Markovian models the state space expansion approach showed great flexibility in terms of modelling capacities. The principal drawback is the explosion of the state space. An attempt to alleviate such problem has been made in [1] but the storing of the reachability graph of the untimed system, augmented with information about active but not enabled events, still remains a bottleneck. This paper suggests a method for storing such an augmented reachability graph by the use of a Multi-terminal Multi-valued Decision Diagram and few Kronecker matrices. All the needed information is collected by applying a Saturation based algorithm that represents the main contribution of the work. An estimation of the memory occupation is also reported. © 2009 Springer-Verlag Berlin Heidelberg.