Please use this identifier to cite or link to this item:
https://cuir.car.chula.ac.th/handle/123456789/79972
| Title: | การตัดไทม์เพทริเน็ตโดยใช้คุณสมบัติตรรกะเชิงเวลาแบบเมตริก |
| Other Titles: | Slicing of time petri nets using metric temporal logic property |
| Authors: | ปฏิมากร จริยฐิติพงศ์ |
| Advisors: | วิวัฒน์ วัฒนาวุฒิ |
| Other author: | จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์ |
| Issue Date: | 2564 |
| Publisher: | จุฬาลงกรณ์มหาวิทยาลัย |
| Abstract: | ไทม์เพทริเน็ตเป็นเครื่องมือสำหรับการสร้างแบบจำลองและทวนสอบระบบเวลาจริง ปริภูมิสถานะของไทม์เพทริเน็ตนั้นมีอัตราการเติบโตแบบเอกโพเนนเชียลเนื่องจากความซับซ้อนของระบบเวลาจริง ซึ่งปริภูมิสถานะที่มีขนาดใหญ่มากอาจทำให้เกิดการระเบิดของปริภูมิสถานะในการทำโมเดลเช็กกิง งานวิจัยนี้จึงนำเสนออัลกอริทึมการตัดไทม์เพทริเน็ตโดยใช้สูตรตรรกะเชิงเวลาแบบเมตริกเพื่อลดขนาดไทม์เพทริเน็ตโดยการกำจัดเพลสและทรานสิชันที่ไม่เกี่ยวข้องกับมาร์คกิงเริ่มต้นและคุณสมบัติของสูตรตรรกะเชิงเวลาแบบเมตริก นอกจากนี้อัลกอริทึมที่นำเสนอยังนำเสนอกราฟพึ่งพาซึ่งแสดงเป็นกราฟพึ่งพาที่แสดงช่วงเวลาโกลบอลของการยิงของทรานสิชันเพื่อแสดงพฤติกรรมการทำงานของไทม์เพทริเน็ต โดยไทม์เพทริเน็ตผลลัพธ์นั้นยังคงเส้นทางการทำงานที่จำเป็นทั้งหมดสำหรับการทำโมเดลเช็กกิง ดังนั้น โมเดลเช็กกิงสามารถสร้างปริภูมิสถานะที่เพียงพอต่อการทวนสอบเมื่อเทียบกับไทม์เพทริเน็ตที่ไม่ได้ตัด |
| Other Abstract: | 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. |
| Description: | วิทยานิพนธ์ (วศ.ด.)--จุฬาลงกรณ์มหาวิทยาลัย, 2564 |
| Degree Name: | วิศวกรรมศาสตรดุษฎีบัณฑิต |
| Degree Level: | ปริญญาเอก |
| Degree Discipline: | วิศวกรรมคอมพิวเตอร์ |
| URI: | http://cuir.car.chula.ac.th/handle/123456789/79972 |
| URI: | http://doi.org/10.58837/CHULA.THE.2021.953 |
| metadata.dc.identifier.DOI: | 10.58837/CHULA.THE.2021.953 |
| Type: | Thesis |
| Appears in Collections: | Eng - Theses |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| 5871414021.pdf | 2.44 MB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.