Automated analysis of DP-systems using timed-arc Petri nets via TAPAAL tool

Timed-Arcs Petri nets (TaPN-nets) are a time extension of Petri nets that allows assigning clocks to tokens. System of dynamic points on a metric graph (DP-systems) is another dynamical model that is studied in discrete geometry dynamics and motivated by study of localized Gaussian wave packets scattering on thin structures; as well, DP-systems could be utilized to overapproximate the dynamics of messages scattering in distributed systems. In the latter case, time-temporal properties of DP-systems become a matter of interest. However, there are no tools that enable us to analyse them. In this work, we provide a new approach to automated analysis of DP-systems using the translation of a DP-system into a TaPN-net which is implemented as a TAPAAL plugin. The translation let us use the comprehensive tool support for TaPN-nets (TAPAAL/UPPAAL) to analyze DP-systems dynamical characteristics expressed in TCTL language. We demonstrated how to express some of them and verify time-temporal properties of a DP-system using the suggested approach, and performed experiments to obtain empirical estimates of the tool performance.