اتوماتون بوچی (زبان انگلیسی: Büchi authortomaton) را می توان به عنوان اتوماتونی در نظر گرفت که می توانند رشته های نامتناهی الفبا را بپذیرد. این اتوماتون اولین بار توسط ژولیوس ریچارد بوچی (Julius Richard Büchi) منطق دان سوئیسی در سال ۱۹۶۲ معرفی شد. اگر ω را به عنوان مجموعه اعداد طبیعی و Σ رابه عنوان الفبا در نظر بگیریم یک کلمه نامتناهی (یا یک ω-کلمه) را می توان به عنوان یک تابع از ω به Σ در نظر گرف...