Chulalongkorn University Theses and Dissertations (Chula ETD)
Other Title (Parallel Title in Other Language of ETD)
Slicing of time petri nets using metric temporal logic property
Year (A.D.)
2021
Document Type
Thesis
First Advisor
วิวัฒน์ วัฒนาวุฒิ
Faculty/College
Faculty of Engineering (คณะวิศวกรรมศาสตร์)
Department (if any)
Department of Computer Engineering (ภาควิชาวิศวกรรมคอมพิวเตอร์)
Degree Name
วิศวกรรมศาสตรดุษฎีบัณฑิต
Degree Level
ปริญญาเอก
Degree Discipline
วิศวกรรมคอมพิวเตอร์
DOI
10.58837/CHULA.THE.2021.953
Abstract
ไทม์เพทริเน็ตเป็นเครื่องมือสำหรับการสร้างแบบจำลองและทวนสอบระบบเวลาจริง ปริภูมิสถานะของไทม์เพทริเน็ตนั้นมีอัตราการเติบโตแบบเอกโพเนนเชียลเนื่องจากความซับซ้อนของระบบเวลาจริง ซึ่งปริภูมิสถานะที่มีขนาดใหญ่มากอาจทำให้เกิดการระเบิดของปริภูมิสถานะในการทำโมเดลเช็กกิง งานวิจัยนี้จึงนำเสนออัลกอริทึมการตัดไทม์เพทริเน็ตโดยใช้สูตรตรรกะเชิงเวลาแบบเมตริกเพื่อลดขนาดไทม์เพทริเน็ตโดยการกำจัดเพลสและทรานสิชันที่ไม่เกี่ยวข้องกับมาร์คกิงเริ่มต้นและคุณสมบัติของสูตรตรรกะเชิงเวลาแบบเมตริก นอกจากนี้อัลกอริทึมที่นำเสนอยังนำเสนอกราฟพึ่งพาซึ่งแสดงเป็นกราฟพึ่งพาที่แสดงช่วงเวลาโกลบอลของการยิงของทรานสิชันเพื่อแสดงพฤติกรรมการทำงานของไทม์เพทริเน็ต โดยไทม์เพทริเน็ตผลลัพธ์นั้นยังคงเส้นทางการทำงานที่จำเป็นทั้งหมดสำหรับการทำโมเดลเช็กกิง ดังนั้น โมเดลเช็กกิงสามารถสร้างปริภูมิสถานะที่เพียงพอต่อการทวนสอบเมื่อเทียบกับไทม์เพทริเน็ตที่ไม่ได้ตัด
Other Abstract (Other language abstract of ETD)
The time Petri net is a powerful tool for modeling and verifying real-time systems. Unfortunately, the state spaces of the time Petri net grow exponentially due to the complexity of real-time systems. The enormous size of the state spaces could also cause state explosion problems in model checking. This dissemination proposes an alternative slicing of the time Petri net algorithm written as a metric temporal logic formula to reduce the size of the time Petri net by eliminating the place and transition sets that are irrelevant to the initial marking and the properties of the metric temporal logic formula. Furthermore, our algorithm proposes an alternative dependency graph representing the global firing time interval of the transition to representing the behavior of the time Petri net. The result preserves all necessary execution paths for the model checking of a particular metric temporal logic formula. Therefore, model checking can generate sufficient state space for verification equivalent to the unsliced time Petri net.
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Recommended Citation
จริยฐิติพงศ์, ปฏิมากร, "การตัดไทม์เพทริเน็ตโดยใช้คุณสมบัติตรรกะเชิงเวลาแบบเมตริก" (2021). Chulalongkorn University Theses and Dissertations (Chula ETD). 5495.
https://digital.car.chula.ac.th/chulaetd/5495