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

Abstract

ไทม์เพทริเน็ตเป็นเครื่องมือสำหรับการสร้างแบบจำลองและทวนสอบระบบเวลาจริง ปริภูมิสถานะของไทม์เพทริเน็ตนั้นมีอัตราการเติบโตแบบเอกโพเนนเชียลเนื่องจากความซับซ้อนของระบบเวลาจริง ซึ่งปริภูมิสถานะที่มีขนาดใหญ่มากอาจทำให้เกิดการระเบิดของปริภูมิสถานะในการทำโมเดลเช็กกิง งานวิจัยนี้จึงนำเสนออัลกอริทึมการตัดไทม์เพทริเน็ตโดยใช้สูตรตรรกะเชิงเวลาแบบเมตริกเพื่อลดขนาดไทม์เพทริเน็ตโดยการกำจัดเพลสและทรานสิชันที่ไม่เกี่ยวข้องกับมาร์คกิงเริ่มต้นและคุณสมบัติของสูตรตรรกะเชิงเวลาแบบเมตริก นอกจากนี้อัลกอริทึมที่นำเสนอยังนำเสนอกราฟพึ่งพาซึ่งแสดงเป็นกราฟพึ่งพาที่แสดงช่วงเวลาโกลบอลของการยิงของทรานสิชันเพื่อแสดงพฤติกรรมการทำงานของไทม์เพทริเน็ต โดยไทม์เพทริเน็ตผลลัพธ์นั้นยังคงเส้นทางการทำงานที่จำเป็นทั้งหมดสำหรับการทำโมเดลเช็กกิง ดังนั้น โมเดลเช็กกิงสามารถสร้างปริภูมิสถานะที่เพียงพอต่อการทวนสอบเมื่อเทียบกับไทม์เพทริเน็ตที่ไม่ได้ตัด