Buechi mu calculus formula explained
The original source is: http://pub.ist.ac.at/gametheory/Lecture4.pdf
I found the proof on the page 5 somewhat unclear, so give here my understanding of it, and also give smaller (but more difficult to remember), formula and proof for the winning set in Buechi games.
Original Formula
The original formula for a winning set in Buechi game is:
\[Y = \nu Y \mu X. [(B \cap Pre_1(Y)) \cup (\neg B \cap Pre_1(X))]\]The idea of the proof is to show that in the winning region \(Y^*\) the first player: a) can always enforce the game to visit a state in \(B\); b) after visiting state in \(B\) the first player can again reach the winning set \(Y^*\). This together means that the first player visits final states infinitely often.
Lets consider the greatest fixpoint first and fix \(Y^*\):
\[Y^* = \mu X. [(B \cap Pre_1(Y^*)) \cup (\neg B \cap Pre_1(X))]\]Let \(T=B \cap Pre_1(Y^*)\), then \(Y^* = \mu X. [T \cup (\neg B \cap Pre_1(X))]\), which reminds the winning set for reachability game, except additional \(\neg B\). It can be shown, for example by contraction, that it is more smaller than reachability set and therefore:
\(Y^* \subseteq \ll 1 \gg (\diamond (B \cap Pre_1(Y^*)))\).
Lets show that from any state in \(Y^*\) the first player can again reach state in \(Y^*\). In the original source this is proved by considering all possible cases: \(x \in T\) and \(x \notin T\), and proving that in both cases the first player can reach \(Y^*\).
But hey, look! Any state in \(Y^*\) can reach \( B \cap Pre_1(Y^*)\), and from the state in \(Pre_1(Y^*)\) the first player can always reach \(Y^*\). Therefore, the the statement is correct and there is no need to consider all cases as in the original source.
OK, we showed that if the first player stays in \(Y^*\), then Buechi condition is satisfied. What about other direction?
Modified Formula
The reasoning above could also apply if we remove \(\neg B\) from the formula. Therefore the formula for the winning set of Buechi game becomes:
\[Y = \nu Y \mu X. [(B \cap Pre_1(Y)) \cup Pre_1(X)]\]Lets check the original proof and see if it works for this case. Again we remove greatest fix point operator by fixing \(Y^*\):
\[Y^* = \mu X. [(B \cap Pre_1(Y^*)) \cup Pre_1(X)]\]Let \(T=B \cap Pre_1(Y^*)\), then \(Y^* = \mu X. [T \cup Pre_1(X)]\), which is the winning set for reachability game, therefore:
\(Y^* = \ll 1 \gg (\diamond (B \cap Pre_1(Y^*)))\).
By using the same argument as for “original formula”, the first player can always reach states in \(Pre_1(Y^*)\) and from there – the state in \(Y^*\). Therefore, the Buechi condition is satisfied and this modified formula represents the winning condition for Buechi game.
The other direction
What if the set \(Y^*\) represents just the subset of the winning set, or even just always empty?
Idea only. It should be possible to prove it by contradiction. Assume there is a state \(x\) from which there is a winning strategy for the first player. Consider the infinite path generated by this state. It contains (at least) one state in \(B\) infinitely often. Then lets make \(Y^* = states-of-that- path\). Such \(Y^*\) satisfies the original formula. Contradiction. Some details are omitted and I am not sure that this way will prove the other direction but would try it first.
Have fun in your learning!