Büchi-Automat

Der Büchi-Automat (nach dem Schweizer Mathematiker Julius Richard Büchi) ist eine spezielle Form des ω-Automaten. Dieser Automatentyp kann benutzt werden, um sowohl Sprachen über unendlichen Wörtern als auch über unendlichen Bäumen zu erkennen.