In the context of the QUANTUM project, whose goal is the development of new quantitative models and quantitative analysis techniques for service-oriented real-time systems that provide the required combinations of probabilistic behavior, real-time behavior, and structure dynamics, we introduced the formal model of Probabilistic Timed Graph Transformation Systems (PTGTSs) and outlined a mapping of PTGTS models employing an extended version of the HENSHIN tool to probabilistic timed automata (PTA) such that the PRISM model checker can be used to analyze PTGTS models with respect to PTCTL properties.
Recently, a simulator for PTGTSs has been developed, to allow for the analysis of complex large-scale PTGTS models.