การตัดไทม์เพทริเน็ตโดยใช้คุณสมบัติตรรกะเชิงเวลาแบบเมตริก

ปฏิมากร จริยฐิติพงศ์

dc.contributor.advisor	วิวัฒน์ วัฒนาวุฒิ
dc.contributor.author	ปฏิมากร จริยฐิติพงศ์
dc.contributor.other	จุฬาลงกรณ์มหาวิทยาลัย. คณะวิศวกรรมศาสตร์
dc.date.accessioned	2022-07-23T05:01:12Z
dc.date.available	2022-07-23T05:01:12Z
dc.date.issued	2564
dc.identifier.uri	http://cuir.car.chula.ac.th/handle/123456789/79972
dc.description	วิทยานิพนธ์ (วศ.ด.)--จุฬาลงกรณ์มหาวิทยาลัย, 2564
dc.description.abstract	ไทม์เพทริเน็ตเป็นเครื่องมือสำหรับการสร้างแบบจำลองและทวนสอบระบบเวลาจริง ปริภูมิสถานะของไทม์เพทริเน็ตนั้นมีอัตราการเติบโตแบบเอกโพเนนเชียลเนื่องจากความซับซ้อนของระบบเวลาจริง ซึ่งปริภูมิสถานะที่มีขนาดใหญ่มากอาจทำให้เกิดการระเบิดของปริภูมิสถานะในการทำโมเดลเช็กกิง งานวิจัยนี้จึงนำเสนออัลกอริทึมการตัดไทม์เพทริเน็ตโดยใช้สูตรตรรกะเชิงเวลาแบบเมตริกเพื่อลดขนาดไทม์เพทริเน็ตโดยการกำจัดเพลสและทรานสิชันที่ไม่เกี่ยวข้องกับมาร์คกิงเริ่มต้นและคุณสมบัติของสูตรตรรกะเชิงเวลาแบบเมตริก นอกจากนี้อัลกอริทึมที่นำเสนอยังนำเสนอกราฟพึ่งพาซึ่งแสดงเป็นกราฟพึ่งพาที่แสดงช่วงเวลาโกลบอลของการยิงของทรานสิชันเพื่อแสดงพฤติกรรมการทำงานของไทม์เพทริเน็ต โดยไทม์เพทริเน็ตผลลัพธ์นั้นยังคงเส้นทางการทำงานที่จำเป็นทั้งหมดสำหรับการทำโมเดลเช็กกิง ดังนั้น โมเดลเช็กกิงสามารถสร้างปริภูมิสถานะที่เพียงพอต่อการทวนสอบเมื่อเทียบกับไทม์เพทริเน็ตที่ไม่ได้ตัด
dc.description.abstractalternative	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.
dc.language.iso	th
dc.publisher	จุฬาลงกรณ์มหาวิทยาลัย
dc.relation.uri	http://doi.org/10.58837/CHULA.THE.2021.953
dc.rights	จุฬาลงกรณ์มหาวิทยาลัย
dc.subject.classification	Computer Science
dc.title	การตัดไทม์เพทริเน็ตโดยใช้คุณสมบัติตรรกะเชิงเวลาแบบเมตริก
dc.title.alternative	Slicing of time petri nets using metric temporal logic property
dc.type	Thesis
dc.degree.name	วิศวกรรมศาสตรดุษฎีบัณฑิต
dc.degree.level	ปริญญาเอก
dc.degree.discipline	วิศวกรรมคอมพิวเตอร์
dc.degree.grantor	จุฬาลงกรณ์มหาวิทยาลัย
dc.identifier.DOI	10.58837/CHULA.THE.2021.953