带有时间戳的着色逻辑Petri网

doi:10.3778/j.issn.1673-9418.2306074

摘要/Abstract

摘要： 针对扩展着色逻辑Petri网存在的表达能力弱以及适用范围窄的问题，提出了一个新的Petri网模型，即带有时间戳的着色逻辑Petri网。首先，将颜色进行实例化以及将变量用于构建有向边上的表达式使得模型能够传递复杂的数据流。其次，引入全局时间以及令牌的时间戳等概念为变迁使能规则增加时间上的约束，使得模型能够用于模拟实时系统。再次，定义库所约束函数并为变迁使能规则增加输出库所上的约束，使得模型能够适用于存储资源有限的场景。接着，提出基于逻辑变迁输入输出矩阵的匹配法，降低逻辑输入变迁的使能判定计算开销并简化逻辑输出变迁的使能判定计算过程。然后，重新定义适用于三类变迁的使能判定条件以及适用于三类库所的标记更新方法，解决原有模型语义在新模型中不适用的问题。最后，通过实例说明新的Petri网模型具有更强的表达能力和适用范围，它能够适用于传递复杂数据流、存储资源有限、实时的且包含批处理选择结构的系统。

关键词: Petri网, 时间戳, 着色令牌, 逻辑变迁

Abstract: Aiming at the problems of weak expressive ability and narrow scope of application in extended colored logical Petri net, timed colored logical Petri net is proposed. Firstly, instantiating colors and using variables to build expressions on directed edges enables the model to transmit complex data flows. Secondly, concepts such as global time and timestamp are introduced to add time constraints to transition enabling rules, so that the model can be used to simulate real-time systems. Thirdly, place restriction functions are defined and constraints on the output places are added to the transition enabling rules, so that the model can be applied to scenes with limited storage resources. Next, a matrix matching method based on logical transition input-output matrix is proposed, which can reduce the calculation cost of the enable decision of the logic input transition and simplify the calculation process of the enable decision of the logic output transition. Then, this paper redefines the enabling rules for three types of transitions and the mark updating methods for three types of places, in order to solve the problem that the semantics of the old model is not applicable to the new model. Finally, an example is given to illustrate that the new Petri net model has stronger expression ability and scope of application, and it can be applied to systems that transmit complex data flows, with limited storage resources, real-time and with batch processing selection structures.

Key words: Petri net, timestamp, colored token, logical transition

王嘉丰, 徐贤. 带有时间戳的着色逻辑Petri网[J]. 计算机科学与探索, 2024, 18(7): 1776-1791.

WANG Jiafeng, XU Xian. Timed Colored Logical Petri Net[J]. Journal of Frontiers of Computer Science and Technology, 2024, 18(7): 1776-1791.

参考文献

[1] VERMA A, PEDROSA L, KORUPOLU M, et al. Large-scale cluster management at Google with Borg[C]//Proceedings of the 10th European Conference on Computer Systems. New York: ACM, 2015: 1-17.
[2] MEDEL V, RANA O, BA?ARES J á, et al. Modelling performance & resource management in kubernetes[C]//Proceedings of the 9th International Conference on Utility and Cloud Computing. New York: ACM, 2016: 257-262.
[3] ABDULLAH M T, QIDRI S, NURYADI W, et al. Failover cluster nodes and ISCSI storage area network on virtualization Windows server 2016[J]. Jurnal Online Informatika, 2020, 5(1): 89-96.
[4] JEFFORD-BAKER J. ALCOL: probabilistic threat modelling of the Amazon elastic container service domain[D]. Stockholm: KTH Royal Institute of Technology, 2019.
[5] JIN X, LI X, ZHANG H, et al. NetChain: scale-free sub-RTT coordination[C]//Proceedings of the 15th USENIX Symposium on Networked Systems Design and Implementation, Renton, Apr 9-11, 2018: 35-49.
[6] LIU Z, BAI Z, LIU Z, et al. DistCache: provable load balancing for large-scale storage systems with distributed caching[C]//Proceedings of the 17th USENIX Conference on File and Storage Technologies, Boston, Feb 25-28, 2019: 143-157.
[7] LENKA R K, PADHI S, NAYAK K M. Fault injection techniques—a brief review[C]//Proceedings of the 2018 International Conference on Advances in Computing, Communication Control and Networking. Piscataway: IEEE, 2018: 832-837.
[8] TASKINSOY J. Typology of stress testing: microprudential vs. macroprudential stress testing of risk exposures[J]. SSRN Electronic Journal, 2019. DOI: 10.2139/ssrn.3361528.
[9] ZAMPETTI F, SCALABRINO S, OLIVETO R, et al. How open source projects use static code analysis tools in continuous integration pipelines[C]//Proceedings of the 2017 IEEE/ACM 14th International Conference on Mining Software Repositories. Piscataway: IEEE, 2017: 334-344.
[10] PASCARELLA L, SPADINI D, PALOMBA F, et al. Information needs in contemporary code review[J]. Proceedings of the ACM on Human-Computer Interaction, 2018, 2: 1-27.
[11] 祝义, 黄志球, 周航. 采用函数式语言的BPEL模型形式化验证方法[J]. 计算机科学与探索, 2018, 12(2): 185-196.
ZHU Y, HUANG Z Q, ZHOU H. Formal method for verifying BPEL model used by functional programming language[J]. Journal of Frontiers of Computer Science and Technology, 2018, 12(2): 185-196.
[12] EICHENBAUM B. The theory of the formal method[J]. Readings in Russian Poetics, 1965: 6.
[13] FAINEKOS G E, PAPPAS G J. Robustness of temporal logic specifications[M]//Formal Approaches to Software Testing and Runtime Verification. Berlin, Heidelberg: Springer, 2006: 178-192.
[14] PETRI C A, REISIG W. Petri net[J]. Scholarpedia, 2008, 3(4): 6477.
[15] VAN DER AALST W M P. Workflow verification: finding control-flow errors using petri-net-based techniques[M]//Business Process Management. Berlin, Heidelberg: Springer, 2000: 161-183.
[16] JENSEN K, KRISTENSEN L M. Colored Petri nets: a graphical language for formal modeling and validation of concurrent systems[J]. Communications of the ACM, 2015, 58(6): 61-70.
[17] JENSEN K, KRISTENSEN L M. Coloured Petri nets: modelling and validation of concurrent systems[M]. Springer Science & Business Media, 2009.
[18] JENSEN K, KRISTENSEN L M, WELLS L. Coloured Petri nets and CPN tools for modelling and validation of concurrent systems[J]. International Journal on Software Tools for Technology Transfer, 2007, 9(3): 213-254.
[19] SOURAVLAS S, KATSAVOUNIS S, ANASTASIADOU S. On modeling and simulation of resource allocation policies in cloud computing using colored Petri nets[J]. Applied Sciences, 2020, 10(16): 5644.
[20] SHAHIDINEJAD A, GHOBAEI-ARANI M, ESMAEILI L. An elastic controller using colored Petri nets in cloud computing environment[J]. Cluster Computing, 2020, 23(2): 1045-1071.
[21] KAID H, AL-AHMARI A, LI Z, et al. Single controller-based colored Petri nets for deadlock control in automated manufacturing systems[J]. Processes, 2019, 8(1): 21.
[22] QI L, LUAN W, LU X S, et al. Shared P-type logic Petri net composition and property analysis: a vector computational method[J]. IEEE Access, 2020, 8: 34644-34653.
[23] LUAN W, QI L, DU Y. Composition of logical Petri nets and compatibility analysis[J]. IEEE Access, 2017, 5: 9152-9162.
[24] LUAN W, QI L, ZHAO Z, et al. Logic Petri net synthesis for cooperative systems[J]. IEEE Access, 2019, 7: 161937-161948.
[25] ZHENG W, DU Y, QI L, et al. A method for repairing process models containing a choice with concurrency structure by using logic Petri nets[J]. IEEE Access, 2019, 7: 13106-13120.
[26] SHA J, DU Y, QI L. A user requirement oriented web service discovery approach based on logic and threshold Petri net[J]. IEEE/CAA Journal of Automatica Sinica, 2019, 6(6): 1528-1542.
[27] LIU L, LIU W, DU Y. Business process modeling and analysis based on queue logical Petri nets[J]. International Journal of Software Engineering and Knowledge Engineering, 2019, 29(1): 115-137.
[28] WANG J, DU Y Y, YU S X. Coloured logic Petri nets and analysis of their reachable trees[J]. Enterprise Information Systems, 2015, 9(8): 900-919.
[29] WANG Z, LUAN W, DU Y, et al. Composition and application of extended colored logic Petri nets to E-commerce systems[J]. IEEE Access, 2020, 8: 36386-36397.