Preview

Труды Института системного программирования РАН

Расширенный поиск

Автоматический анализ дискретных динамических систем на метрических графах с помощью сетей Петри с временными дугами и инструмента TAPAAL

https://doi.org/10.15514/ISPRAS-2020-32(6)-12

Полный текст:

Аннотация

Сети Петри с временными дугами – это временное расширение сетей Петри (TaPN-сети), которое позволяет присваивать таймеры фишкам. Система динамических точек на метрическом графе (DP-система) это другая динамическая модель, которая рассматривается в теории геометрических дискретных динамических систем и, исторически, ее изучение мотивировано изучением распространения локализованных гауссовых волновых пакетов по тонким структурам; кроме того, DP-системы могут использоваться для приближенного представления динамики распространения сообщений в распределенных системах. В этой работе, мы описываем новый подход для автоматического анализа DP-систем используя трансляцию в TaPN сеть, которая реализована как расширение инструмента TAPAAL. Подход позволяет использовать мощные инструменты верификации (TAPAAL/UPPAAL) для анализа динамических характеристик DP-систем, представленных на языке TCTL. В работе продемонстрировано, как можно кодировать временно-темпоральные свойства DP-систем в рамках предложенного подхода, и приведены результаты экспериментальных тестов.

Об авторах

Леонид Владимирович ДВОРЯНСКИЙ
Фрилансер
Россия
Доктор естественных наук (Doctor rerum naturalium), независимый исследователь


Александр Александрович ИЗМАЙЛОВ
Национальный исследовательский университет «Высшая школа экономики»
Россия
Проходит обучение в департаменте программной инженерии факультета компьютерных наук


Список литературы

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.


Для цитирования:


ДВОРЯНСКИЙ Л.В., ИЗМАЙЛОВ А.А. Автоматический анализ дискретных динамических систем на метрических графах с помощью сетей Петри с временными дугами и инструмента TAPAAL. Труды Института системного программирования РАН. 2020;32(6):155-166. https://doi.org/10.15514/ISPRAS-2020-32(6)-12

For citation:


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

Просмотров: 67


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)