Automated Analysis of DP-systems Using Timed-Arc Petri Nets via TAPAAL Tool
https://doi.org/10.15514/ISPRAS-2020-32(6)-12
Abstract
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.
Supporting agencies: This work was supported by the RFBR grant 20-07-01103 a.
About the Authors
Leonid Wladimirovich DWORZANSKI
Freelancer
Russian Federation
Doctor of natural sciences (Doctor rerum naturalium), independent researcher
Russian Federation
Doctor of natural sciences (Doctor rerum naturalium), independent researcher
Aleksandr Aleksandrovich IZMAYLOV
National Research University Higher School of Economics
Russian Federation
Studies at School of Software Engineering Faculty of Computer Science
Russian Federation
Studies at School of Software Engineering Faculty of Computer Science
References
1. Reisig W. Understanding Petri Nets – Modeling Techniques, Analysis Methods, Case Studies. Springer, 2013, 257 p.
2. Hanisch H.-M. Analysis of place/transition nets with timed arcs and its application to batch process control. Lecture Notes in Computer Science, vol. 691, 1993, pp. 282–299.
3. Berkolaiko G. and Kuchment P. Introduction to quantum graphs. American Mathematical Society, 2013, 270 p
4. Berkolaiko G., Carlson R., Fulling S. A., Kuchment P., eds. Quantum Graphs and Their Applications. Proc. of an AMS-IMS-SIAM Joint Summer Research Conference on Quantum Graphs and Their Applications. American Mathematical Society, 2006, 307 p.
5. Чернышев В.Л. Нестационарное уравнение Шрёдингера:статистика распространения гауссовых пакетов на геометрическом графе. Труды Математического института им. В.А. Стеклова, том 270, 2010 г., стр. 249–265 / Chernyshev V. L. Time-dependent Schrödinger equation: Statistics of the distribution of Gaussian packets on a metric graph. Proceedings of the Steklov Institute of Mathematics, vol. 270, 2010, pp. 246–262.
6. Tolchennikov A.A., Chernyshev V.L., Shafarevich A.I. Behavior of quasi-particles on hybrid spaces. relations to the geometry of geodesics and to the problems of analytic number theory. Regular and Chaotic Dynamics, vol. 21, no. 5, 2016, pp. 531–537.
7. Exner P. and Lipovsky J. Topological bulk-edge effects in quantum graph transport. Physics Letters A, vol. 384, issue 18, 2020, article id 126390.
8. Толченников А.А., Чернышев В.Л., Шафаревич А.И. Асимптотические свойства и классические динамические системы в квантовых задачах на сингулярных пространствах. Нелинейная динамика, том 6, no. 3, 2010 г, стр. 623-638 A. A. Tolchennikov, V. L. Chernyshev, A. I. Shafarevich, Asymptotic properties and classical dynamical systems in quantum problems on singular spaces, Russian Journal of Nonlinear Dynamics, vol. 6, no. 3, 2010, pp. 623–638 (in Russian).
9. Chernyshev V.L., Tolchennikov A.A. Asymptotic estimate for the counting problems corresponding to the dynamical system on some decorated graphs. Ergodic Theory and Dynamical Systems, vol. 38, no. 5, 2018, pp. 1697–1708.
10. Chernyshev V.L., Tolchennikov A.A. Correction to the leading term of asymptotics in the problem of counting the number of points moving on a metric tree. Russian Journal of Mathematical Physics, vol. 24, no. 3, 2017, pp. 290–298.
11. Chernyshev V.L., Tolchennikov A.A. The second term in the asymptotics for the number of points moving along a metric graph. Regular and Chaotic Dynamics, vol. 22, no. 8, 2017, pp. 937–948.
12. Bolognesi T., Lucidi F., and Trigila S. From timed Petri nets to timed LOTOS. In Proc. of the IFIP WG6. 1 Tenth International Symposium on Protocol Specification, Testing and Verification X, 1990, pp. 395–408.
13. David A., Jacobsen L., Jacobsen M., Jørgensen K., Møller M., and Srba J. TAPAAL 2.0: integrated development environment for timed-arc Petri nets. Lecture Notes in Computer Science, vol. 7214, 2012, pp. 492–497.
14. Model checking contest 2020. Available at: https://mcc.lip6.fr/models.php, accessed June 2020.
15. Esparza J. Decidability and complexity of Petri net problems – an introduction. Lecture Notes in Computer Science, vol. 1491, 1998, pp. 374–428.
16. Czerwinski W., Lasota S., Lazic R., Leroux J., Mazowiecki F. The reachability problem for Petri nets is not elementary. In Proc. of the 51st Annual ACM SIGACT Symposium on Theory of Computing, 2019, pp. 24–33.
17. Berard B., Cassez F., Haddad S., Lime D., and Roux O. H. Comparison of different semantics for time Petri nets. Lecture Notes in Computer Science, vol. 3703, 2005, pp. 293–307.
18. Brown C. and Gurr D. Timing Petri nets categorically. Lecture Notes in Computer Science, vol. 623, 1992, pp. 571–582.
19. Merlin P. A study of the recoverability of computer systems. Ph. D. Thesis, Dept. of Information and Computer Science, University of California, Irvine, CA, 1974.
20. Ramchandani C. Analysis of asynchronous concurrent systems by timed Petri nets. Ph. D. Thesis, Dept. of Electrical Engineering, Massachusetts Institute of Technology, Cambridge, 1974.
21. Tvardovskii A.S., Yevtushenko N.V. On reduced forms of initialized Finite State Machines with timeouts. Trudy ISP RAN/Proc. ISP RAS, vol. 32, issue 2, 2020, pp. 125-134. DOI: 10.15514/ISPRAS-2020-32(2)-10.
22. Твардовский А.С., Лапутенко А.В. О возможностях автоматного описания параллельной композиции временных автоматов. Труды ИСП РАН, том 30, вып. 1, 2018 г., стр. 25-40 / Tvardovskii A.S., Laputenko A.V. On the possibilities of FSM description of parallel composition of timed Finite State Machines. Trudy ISP RAN/Proc. ISP RAS, vol. 30, issue 1, 2018, pp. 25-40 (in Russian). DOI: 10.15514/ISPRAS-2018-30(1)-2.
23. Vinarskii E.M., Zakharov V.A. On the verification of strictly deterministic behaviour of Timed Finite State Machines. Trudy ISP RAN/Proc. ISP RAS, vol. 30, issue 3, 2018, pp. 325-340. DOI: 10.15514/ISPRAS-2018-30(3)-22.
24. Akshay S., Genest B., and Helouet L. Decidable Classes of Unbounded Petri Nets with Time and Urgency. In Proc. of the 37th International Conference on Application and Theory of Petri Nets and Concurrency, 2016, pp. 301–322.
25. Dworzanski L.W. Bounding untimed Petri net using timing operation. Report on doctoral intermediate thesis results, 2013-09-16. Available at http://mathtech.ru/dworzanski/talks/bounding.html
26. Dworzanski L.W. Consistent timed semantics for nested Petri nets with restricted urgency. Lecture Notes in Computer Science, vol. 9884, 2016, pp. 3-18.
27. Jacobsen L., Jacobsen M., Møller M. H., Srba J. Verification of timed-arc Petri nets. Lecture Notes in Computer Science, vol.6543, 2011, pp. 46-72.
28. Shoshmina I.V. Developing formal temporal requirements to distributed program systems. System informatics, no. 8, 2016, pp. 21-32.
29. Alur R, Courcoubetis C, Dill D. Model-checking in dense real-time. Information and Computation, vol. 104, no. 1, 1993, pp. 2-34.
30. Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем. БХВ-Петербург, 2010 г., 552 стр. / Karpov Yu. G., Model checking. Verification of parallel and distributed systems. BHV-Peterburg, 2010, 552 p. (in Russian).
31. JSON Graph Format (JGF). Available at: http://jsongraphformat.info, accessed November 2020.
32. yEd Graph Editor: High-quality diagrams made easy. Available at: https://www.yworks.com/products/yed, accessed November 2020.
Review
For citations:
DWORZANSKI L.W., IZMAYLOV A.A. Automated Analysis of DP-systems Using Timed-Arc Petri Nets via TAPAAL Tool. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2020;32(6):155-166. https://doi.org/10.15514/ISPRAS-2020-32(6)-12
Email this article 