Półdeterministyczny automat Büchiego