Chulalongkorn University Theses and Dissertations (Chula ETD)
Other Title (Parallel Title in Other Language of ETD)
Transformation of kripke structure with linear temporal logic formula to büchi automata
Year (A.D.)
2023
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.2023.988
Abstract
โดยทั่วไปโครงสร้างคริปกี หรือที่รู้จักกันในนามของระบบทรานสิชันที่ถูกนำมาใช้เพื่อแสดงสถานะจำกัด และการเปลี่ยนแปลงในระบบที่ไม่มีที่สิ้นสุด โดยที่โครงสร้างคริปกีนั้นจะไม่มีสถานะยอมรับหรือเรียกว่าสถานะสิ้นสุด เมื่อต้องทำการดำเนินการทวนสอบด้วยโมเดลเช็กกิงด้วยสูตรตรรกะเชิงเวลาแบบลำดับ จากคุณสมบัติและการพิจารณาการตรวจสอบความว่างเปล่าจากเทคนิคการจำกัด โครงสร้างคริปกีที่ถูกกำหนดต้องถูกแปลงไปอยู่ในรูปแบบของบูชีออโตมาตาที่สอดคล้องกันเสียก่อน ในการแปลงนั้นเพื่อแน่ใจว่าผลลัพธ์บูชีออโตมาตาที่มีสถานะยอมรับเหมาะสมสำหรับการตรวจสอบความว่างเปล่าโดยการใช้บูชีออโตมาตาที่ได้จากสูตรตรรกะเชิงเวลาแบบลำดับที่แสดงคุณสมบัติที่ต้องการ ในงานวิจัยนี้ได้นำเสนออีกทางเลือกในการแปลงโครงสร้างคริปกีที่กำหนดโดยพร้อมกับสูตรตรรกะเชิงเวลาแบบลำดับที่จะแสดงถึงคุณสมบัติที่ต้องการให้กลายเป็นบูชีออโตมาตาที่สอดคล้องกันที่มีสถานะยอมรับในจำนวนที่เพียงพอตามสูตรตรรกะเชิงเวลาแบบลำดับ วิธีการนี้จะช่วยลดความซับซ้อนของกระบวนการ เพิ่มความชัดเจนของโครงสร้างทั้งหมด ทำให้การตีความ การวิเคราะห์เงื่อนไขของพฤติกรรมที่ต้องการของระบบได้ง่ายขึ้น โดยการทวนสอบด้วยโมเดลเช็กกิงกับบูชีออโตมาตาที่ได้จากการแปลงที่มีสถานะยอมรับสอดคล้องกับสูตรตรรกะเชิงเวลาแบบลำดับที่ต้องการ เราก็สามารถประเมินความน่าพอใจของคุณสมบัติเหล่านั้นได้อย่างแม่นยำ
Other Abstract (Other language abstract of ETD)
In general, a Kripke structure, also known as a transition system, is utilized to represent the finite states and their transitions in an infinite execution system. Traditional Kripke structures do not include accepting states. When performing model checking for linear temporal logic (LTL) properties and considering emptiness checking in the automata language containment technique, the given Kripke structure needs to be transformed into a corresponding Büchi automata. This transformation ensures that the resulting Büchi automata are assigned with appropriate accepting states for the subsequent emptiness checking with the second Büchi automata derived from the LTL formula representing the desired properties. In this paper, an alternative approach to transform the given Kripke structure is proposed, together with the LTL formula representing the desired properties, into a corresponding Büchi automata with the adequate numbers of accepting states based on the provided LTL formula. It apparently reduces complexity and increases clarity of the overall structure and make easier to interpret and reason about the acceptance conditions and the desired behaviors of the system. By performing model checking on these modified Büchi automata, which now have the appropriate accepting states and correspond to the desired LTL formula properties, we can accurately assess their satisfiability.
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Recommended Citation
รุ่งเศรษฐพัฒน์, ณัฏฐ์, "การแปลงโครงสร้างคริปกีพร้อมด้วยสูตรตรรกะเชิงเวลาแบบลำดับเป็นบูชีออโตมาตา" (2023). Chulalongkorn University Theses and Dissertations (Chula ETD). 11619.
https://digital.car.chula.ac.th/chulaetd/11619
