Decidability method of Petri net non-reachability marks and its application in deadlock detection

doi:10.13196/j.cims.2016.02.019

›› 2016, Vol. 22 ›› Issue (第2期): 465-475.DOI: 10.13196/j.cims.2016.02.019

Previous Articles Next Articles

Decidability method of Petri net non-reachability marks and its application in deadlock detection

Online:2016-02-29 Published:2016-02-29
Supported by:
Project supported by the National Natural Science Foundation,China(No.61170079,61202152,61472229,61502279),the S &T Development Fund of Shandong Province,China(No.2014GGX101035,ZR2015FM013),the Scientific Research Award Foundation for Outstanding Young Scientists of Shandong Province,China(No.BS2014DX013),the Open Project Foundation of Key Laboratory of Embedded System and Service Computing,Ministry of Education,Tongji University,China(No.ESSCKF201403),the SDUST Research Fund,China,and the Domestic Visiting Scholars Program for Young Teachers of Shandong Colleges and Universities,China.

Petri网不可达标识的判定方法研究及其在死锁检测中的应用

鲁法明^1,2,曾庆田³⁺,段华⁴,彭延军¹,包云霞⁴

1.山东科技大学信息科学与工程学院
2.同济大学嵌入式系统与服务计算教育部重点实验室
3.山东科技大学电子通信与物理学院
4.山东科技大学数学与系统科学学院

基金资助:
国家自然科学基金资助项目(61170079,61202152,61472229,61502279);山东省科技发展资助项目(2014GGX101035,ZR2015FM013);山东省优秀中青年科学家科研奖励基金资助项目(BS2014DX013);同济大学嵌入式系统与服务计算教育部重点实验室开放课题基金资助项目(ESSCKF201403);山东科技大学科研创新团队支持计划与领军人才计划资助项目;山东省高等学校青年骨干教师国内访问学者资助项目。

Abstract

Abstract: To make deadlock detection,the method for non-reachability decidability in specific mark of Petri net was researched.The decision method for non-reachability was analyzed based on solution existence of state equations and structural characteristics such as siphons,traps,S-invariants,modular S-invariants.The relationship of those non-reachable marks which could be decided through different non-reachability analysis method was discussed.A taxonomic hierarchy of Petri net non-reachable marks was established,which provided theoretical support for non-reachability decidability.In addition,the proposed method was applied to detect the deadlock state of two Petri nets which were used to model the dining philosophers problem and a cross-organizational collaborative business processes.

Key words: Petri nets, reachability analysis, non-reachable marks classification, deadlock detection

摘要： 为进行系统死锁检测,对Petri网特定标识的不可达性判定方法进行研究。对基于虹吸管、陷阱、S-不变量、加模S-不变量等结构特性以及基于状态方程解存在性的不可达标识判定方法进行分析,研究了上述方法可以判定的不可达标识之间的相互关系,建立了Petri网不可达标识的分类体系,为更好地进行标识不可达性判定提供了理论依据。分别结合哲学家就餐问题和一个跨组织协同业务流程Petri网模型的死锁状态,检测说明了标识不可达判定方法的应用。

关键词: Petri网, 可达性分析, 不可达标识分类, 死锁检测

CLC Number:

TP301

鲁法明,曾庆田,段华,彭延军,包云霞. Petri网不可达标识的判定方法研究及其在死锁检测中的应用[J]. 计算机集成制造系统, 2016, 22(第2期): 465-475.

[1]	. Deadlock detection method based on Petri net mining of program trajectory [J]. , 2021, 27(9): 2611-2624.
[2]	. Dynamic decision-making of manufacturing resource based on digital twin [J]. , 2021, 27(2): 521-535.
[3]	. Modeling and simulation for enterprises' RFID adoption and internalization based on stochastic Petri nets [J]. , 2020, 26(第2): 470-480.
[4]	. Petri net-based hierarchical business process mining [J]. , 2020, 26(6): 1525-1537.
[5]	. Analyzing realizability of choreographies using Petri nets [J]. , 2020, 26(6): 1548-1556.
[6]	. Business alignments based on reachable graphs of Petri nets [J]. , 2020, 26(6): 1589-1606.
[7]	. Aligning event logs and process models based on Petri nets [J]. , 2019, 25(第4): 809-829.
[8]	. Conformance checking of business process based on artifact lifecycle mode [J]. , 2019, 25(第4): 856-863.
[9]	. Process mining approach of discovering behavior blocks based on successor relation [J]. , 2019, 25(第4): 901-908.
[10]	. Matching mechanism of physical and information processes in discrete series production system [J]. , 2019, 25(第11): 2923-2934.
[11]	. Failure response policy for revisiting dual-arm cluster tools based on Petri nets [J]. , 2019, 25(12): 3235-3246.
[12]	. Solving algorithm for scheduling problem with control-flow constraints [J]. , 2018, 24(第7): 1598-1607.
[13]	. Extending α-algorithm to mine simplest 2-Loops [J]. , 2018, 24(第3): 591-601.
[14]	. Multiple die and composite geometry machining process simulation technology for bending machine [J]. , 2018, 24(第1): 19-33.
[15]	. Business process modeling and analysis based on logical data Petri net [J]. , 2017, 23(第5期): 921-930.

Decidability method of Petri net non-reachability marks and its application in deadlock detection

Petri网不可达标识的判定方法研究及其在死锁检测中的应用

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics