Causal Semantics for Time Petri Nets with Weak Time Policy
DOI:
https://doi.org/10.14529/cmse260103Keywords:
time Petri net, weak time elapsing policy, time process, causal semanticsAbstract
Time Petri Nets (TPNs) are an extension of classical Petri Nets designed for modeling and analyzing concurrent and distributed systems with respect to real-time characteristics. In TPNs, transitions representing system events have local clocks and firing time intervals. Two time-elapsing policies are considered for this model: the strong policy, where the progress of time is blocked by the necessity of a transition firing, and the weak policy, which does not restrict the progress of model time. These policies are incomparable in expressive power, and many standard verification problems are decidable only for the weak policy. In the general case, the state space of TPNs is infinite and uncountable, which complicates the analysis of model behavior. To reduce the state space, causal semantics is applied, describing system behavior through a partial order relation on the set of events. This approach allows for abstraction from the redundant set of all possible event interleavings while preserving information about causal dependencies and concurrency between system events. The paper introduces a model of time processes that represents causal semantics for TPNs in the context of the weak time policy. The main result of the work is the establishment of a bijective correspondence between TPN runs (representing classical interleaving semantics) and linearizations of time processes, which proves the correctness of the proposed causal semantics. Computational experiments presented in the paper confirm a significant reduction in the analyzed state space of TPNs when using time processes.References
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.
