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

จากวิกิพีเดีย สารานุกรมเสรี
Jump to navigation Jump to search

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

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

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

  •  : เซตจำกัด ของอักษร
  •  : เซตของคำจำกัด
  •  : เซตของคำ (-words หรือ -sequences )

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

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

เราเรียกการยอมรับคำแบบนี้ว่าการยอมรับแบบบือคี (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