บือคีออโตมาตอน

บือคีออโตมาตอน (Büchi automaton) ตั้งชื่อตาม Julius Richard Büchi นักคณิตศาสตร์ชาวสวิส ใช้สำหรับการคำนวณซึ่งมีลักษณะเป็นอนันต์ คือการคำนวณนั้นดำเนินเรื่อยไปไม่มีสิ้นสุด การประยุกต์ใช้บือคีออโตมาตานั้น มีตัวอย่างในด้าน formal method เช่น ตรรกและการให้เหตุผลในระบบรีแอคทีฟ (reactive system) และ การตรวจสอบโมเดล (model checking)

สัญลักษณ์

สัญลักษณ์ที่ใช้ในหัวข้อนี้:

• ${\displaystyle A}$  : เซตจำกัด ของอักษร
• ${\displaystyle A^{*}}$  : เซตของคำจำกัด
• ${\displaystyle A^{\omega }}$  : เซตของคำ${\displaystyle \omega }$  (${\displaystyle \omega }$ -words หรือ ${\displaystyle \omega }$ -sequences )

บือคีออโตมาตอน

บือคีออโตมาตอน เป็น NFA ซึ่งมีการปรับเปลี่ยนเงื่อนไงการยอมรับ เพื่อรองรับ คำ ${\displaystyle \omega }$ . การยอมรับคำ ${\displaystyle \omega }$  ของ บือคีออโตมาตอนเกิดขึ้นเมื่อ อ่านคำซึ่งอินพุตจากซ้ายไปขวาและทำการเปลี่ยนสถานะตาม ที่กำหนดโดยฟังก์ชันการเปลี่ยนสถานะ แล้วในสายลำดับการเปลี่ยนสถานะนั้น มีสถานะยอมรับเกิดขึ้นบ่อยเป็นอนันต์

เราเรียกการยอมรับคำแบบนี้ว่าการยอมรับแบบบือคี (Büchi acceptance)

อ้างอิง

• Wolfgang THOMAS, Automata on Infinite Objects, Handbook of theoretical computer science (vol. B): formal models and semantics, ISBN 0-444-88074-7