Previous chapter: Semi-Deterministic Büchi Automata
This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner
Introduction
From the semi-deterministic Büchi automaton we now build a deterministic Muller automaton. The idea of the construction is to continuously simulate, in the deterministic automaton, the nondeterministic part of the semi-deterministic automaton and to ”attempt” a transition into the deterministic part whenever possible.
In the state of the deterministic automaton we maintain an “array” of states that correspond to these attempts. Along each run of the automaton, there may of course be infinitely many such attempts; we only need a finite array, however, because we do not need to keep track of two different attempts to enter the deterministic part, if they both reach the same state (in this case, we simply track the attempt that entered the deterministic part earlier).
We use an array of size $2m$, where m is the number of states of the deterministic part. The factor two allows us to leave a position of the array empty (“␣”) if an attempt is not continued. This is necessary to distinguish a situation where a previously started attempt failed and, at the same time, a new attempt enters the deterministic part, from the situation where the same attempt ran continuously. The deterministic automaton accepts if there is at least one attempt that runs forever after some point and reaches an accepting state infinitely often.
Next chapter: Infinite Games (Basic Definitions)
Please cite the source for reprints, feel free to verify the sources cited in the article, and point out any errors or lack of clarity of expression. You can comment in the comments section below or email to GreenMeeple@yahoo.com