As a part of the QUANTUM project, we developed the formal model of Probabilistic Timed Graph Transformation Systems (PTGTSs) as a means for modeling and analysis of systems with timed behavior, probabilistic behavior, and structure dynamics.
In the context of the QUANTUM project, we already provided model checking support for PTGTSs. However, with PTGTS being especially well-suited for modeling and analysis of complex systems of systems, which naturally appear in large-scale topologies, model checking approaches that are limited to the analysis of only small or medium size models are often insufficient.
To close this gap, we developed a simulator for PTGTSs that can import real-world topologies, automatically detect violations of state properties during the simulation runs, and handle the graph pattern matching as well as time and probabilities efficiently so that complex large-scale topologies can be considered.
The concepts behind our simulator are presented in the tool paper "A Simulator for Probabilistic Timed Graph Transformation Systems with Complex Large-Scale Topologies", which was accepted at ICGT 2020.
As an addition to the aforementioned tool paper, we offer a high-level description of our simulator implementation (PDF) to interested readers.
The source code of the simulator will be made available here soon.