Причинно-следственная семантика для непрерывно-временных сетей Петри со слабой временной стратегией

Алексей Юрьевич Зубарев
Институт систем информатики им. А.П. Ершова СО РАН, Новосибирск


Аннотация


Непрерывно-временные сети Петри (НВСП) являются расширением классических сетей Петри, предназначенным для моделирования и анализа параллельных и распределенных систем с учетом временных характеристик. В НВСП переходы, моделирующие события системы, имеют локальные часы и временные интервалы срабатывания. Для данной модели рассматриваются две стратегии хода времени: сильная, при которой ход времени блокируется необходимостью срабатывания перехода, и слабая, не ограничивающая ход модельного времени. Эти стратегии несравнимы по выразительности, причем многие стандартные задачи анализа разрешимы лишь для слабой стратегии. В общем случае пространство состояний НВСП бесконечно и несчетно, что усложняет анализ поведения модели. Для редукции пространства рассматриваемых состояний применяется причинно-следственная семантика, описывающая поведение системы через отношение частичного порядка на множестве событий. Данный подход позволяет абстрагироваться от избыточного множества всех возможных чередований событий (интерливинга), а также сохраняет информацию о причинно-следственных связях и параллелизме между событиями системы. В статье определяется и исследуется модель временных процессов, представляющая причинно-следственную семантику для НВСП в контексте слабой временной стратегии. Основным результатом работы является установление взаимооднозначного соответствия между пробегами НВСП (представляющими классическую интерливинговую семантику) и линеаризациями временных процессов, что доказывает корректность предложенной причинно-следственной семантики. Представленные в работе вычислительные эксперименты подтверждают значительную редукцию пространства анализируемых состояний НВСП при использовании временных процессов.

Ключевые слова


непрерывно-временная сеть Петри; слабая стратегия хода времени; временной процесс; причинно-следственная семантика

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

PDF

Литература


Komenda J., Lefebvre D. On tick automata for distributed timed DESs with synchronisations and minimal time constraints. IFAC-PapersOnLine. 2023. Vol. 56, no. 2. P. 8635–8640.DOI: 10.1016/j.ifacol.2023.10.039.

Boyer M., Roux O.H. Comparison of the expressiveness of arc, place and transition time Petri nets. 28th International Conference on Applications and Theory of Petri Nets, ICATPN 2007, Siedlce, Poland, June 25–29, 2007. Vol. 4546. Berlin, Heidelberg, Springer, 2007. P. 63–82. Lecture Notes in Computer Science. DOI: 10.1007/978-3-540-73094-1_7.

Komenda J., Lahaye S., Parrot R., Roux O.H. Weakly strong semantics of time Petri nets for performance evaluations. IFAC-PapersOnLine. 2024. Vol. 58, no. 1. P. 66–71. DOI: 10.1016/j.ifacol.2024.07.012.

B´erard B., Cassez F., Haddad S., et al. Comparison of the expressiveness of timed automata and time Petri nets. 3rd International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2005, Uppsala, Sweden, September 26–28, 2005. Vol. 3829. Berlin, Heidelberg, Springer, 2005. P. 211–225. Lecture Notes in Computer Science. DOI: 10.1007/11603009_17.

Reynier P.A., Sangnier A. Weak time Petri nets strike back! 20th International Conference on Concurrency Theory, CONCUR 2009, Bologna, Italy, September 1–4, 2009. Vol. 5710. Berlin, Heidelberg, Springer, 2009. P. 557–571. Lecture Notes in Computer Science. DOI: 10.1007/978-3-642-04081-8_37.

Lime D., Parrot R., Roux O.H. Decidability problems for weak time Petri nets with read, reset and transfer arcs. 46th International Conference on Application and Theory of Petri Nets and Concurrency, Petri Nets 2025, Paris, France, June 23–27, 2025. Vol. 15714. Cham, Springer, 2025. P. 289–308. Lecture Notes in Computer Science. DOI: 10.1007/978-3-031-94634-9_16.

Leclercq L., Lime D., Roux O.H. A state class based controller synthesis approach for time Petri nets. 44th International Conference on Application and Theory of Petri Nets and Concurrency, Petri Nets 2023, Lisbon, Portugal, June 25–30, 2023. Vol. 13929. Cham, Springer, 2023. P. 409–429. Lecture Notes in Computer Science. DOI: 10.1007/978-3-031-33620-1_21.

Hadjidj R. An efficient approach for model-checking zeno behaviors in real-time system models based on the time Petri net formalism. IEEE Transactions on Automation Science and Engineering. 2024. Vol. 21, no. 4. P. 6628–6642. DOI: 10.1109/TASE.2023.3328895.

Godary-Dejean K., Leroux H., Andreu D. Interpreted synchronous extension of time Petri nets. Discrete Event Dynamic Systems. 2022. Vol. 32. P. 27–64. DOI: 10.1007/s10626-021-00347-z.

Aura T., Lilius J. A causal semantics for time Petri nets. Theoretical Computer Science. 2000. Vol. 243. P. 409–447. DOI: 10.1016/S0304-3975(99)00114-0.

Zubarev A. State space reduction for time Petri nets with weak semantics. Bulletin of the Novosibirsk Computing Center. Series: Computer Science. 2019. No. 43. P. 39–52. DOI: 10.31144/bncc.cs.2542-1972.2019.n43.p39-52.

Heiner M., Gilbert D., Donaldson R. Petri nets for systems and synthetic biology. 8th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2008, Bertinoro, Italy, June 2–7, 2008. Vol. 5016. Berlin, Heidelberg, Springer, 2008. P. 215–264. Lecture Notes in Computer Science. DOI: 10.1007/978-3-540-68894-5_7.

Szawulak B., Radom M., Formanowicz P. Comparison by partition—Finding Petri nets similarity on the basis of subnets. Computers in Biology and Medicine. 2025. Vol. 187. Art. 109775. DOI: 10.1016/j.compbiomed.2025.109775.

Olszak J., Radom M., Formanowicz P. Some aspects of modeling and analysis of complex biological systems using time Petri nets. Bulletin of the Polish Academy of Sciences. Technical Sciences. 2018. Vol. 66, no. 1. P. 67–78. DOI: 10.24425/119060.

Gilin V., Laauwen S., Xia Y., et al. Modeling HIF-ILK interaction using continuous Petri nets. 18th Biomedical Engineering Systems and Technologies, BIOSTEC 2025, Porto, Portugal, February 20–22, 2025, Proceedings of the 18th International Joint Conference. Set´ubal, SCITEPRESS, 2025. P. 537–544. DOI: 10.5220/0013102600003911.

Gilbert D., Heiner M. From Petri Nets to Differential Equations — An Integrative Approach for Biochemical Network Analysis. 27th International Conference on Applications and Theory of Petri Nets and Other Models of Concurrency, ICATPN 2006, Turku, Finland, June 26–30, 2006. Vol. 4024. Berlin, Heidelberg, Springer, 2006. P. 200–219. Lecture Notes in Computer Science. DOI: 10.1007/11767589_11.

Grieco L., Calzone L., Bernard-Pierrot I., et al. Integrative modelling of the influence of MAPK network on cancer cell fate decision. PLoS Computational Biology. 2013. Vol. 9, no. 10. DOI: 10.1371/journal.pcbi.1003286.

Sahin O., Frohlich H., Lobke C., et al. Modeling ERBB receptor-regulated G1/S transition to find novel targets for de novo trastuzumab resistance. BMC Systems Biology. 2009. Vol. 3, no. 1. P. 1–20. DOI: 10.1186/1752-0509-3-1.

Kordon F., Hulin-Hubard F., Jezequel L., et al. Complete results for the 2025 edition of the Model Checking Contest. 2025. URL: https://mcc.lip6.fr/2025/results.php (accessed: 14.12.2025).

Virbitskaite I.B., Bushin D., Best E. True concurrent equivalences in time Petri nets. Fundamenta Informaticae. 2016. Vol. 149. P. 401–418. DOI: 10.3233/FI-2016-1454.




DOI: http://dx.doi.org/10.14529/cmse260103