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

จากวิกิพีเดีย สารานุกรมเสรี

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

สัญลักษณ์[แก้]

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

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

บือคีออโตมาตอน[แก้]

บือคีออโตมาตอน เป็น NFA ซึ่งมีการปรับเปลี่ยนเงื่อนไงการยอมรับ เพื่อรองรับ คำ \omega. การยอมรับคำ \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