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

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

Please use this identifier to cite or link to this item: https://cuir.car.chula.ac.th/handle/123456789/79972

Full metadata record

DC Field	Value	Language
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	-
Appears in Collections:	Eng - Theses

Files in This Item:

File	Description	Size	Format
5871414021.pdf		2.44 MB	Adobe PDF	View/Open

Show simple item record