Tree Automata, Mu-Calculus and Determinacy (Extended Abstract)

Tree Automata, Mu-Calculus and Determinacy (Extended Abstract)

| E.A. Emerson^1 and C.S. Jutla^2
The paper by E.A. Emerson and C.S. Jutla explores the equivalence between the propositional Mu-Calculus and finite automata on infinite trees, providing a simplified proof of Rabin's Complementation Lemma for tree automata. The authors show that the Mu-Calculus is equivalent in expressive power to tree automata, which trivially implies that tree automata are closed under complementation. This equivalence is demonstrated by translating the parse tree of a Mu-Calculus formula into an alternating tree automaton, and then reducing this to a nondeterministic tree automaton. The paper also discusses how the Mu-Calculus can be used to establish the determinacy of certain infinite games, including those used in the theory of on-line algorithms. The authors provide a detailed construction for translating Mu-Calculus formulas into equivalent tree automata and prove the determinacy of infinite games with parity winning conditions. They also show that if a player has a winning strategy in a parity infinite game, then the player has a history-free winning strategy. Finally, the paper discusses the determinacy of on-line games and provides a Mu-Calculus characterization for $F_\sigma$ games, simplifying the proof of de-randomization of competitive on-line algorithms.The paper by E.A. Emerson and C.S. Jutla explores the equivalence between the propositional Mu-Calculus and finite automata on infinite trees, providing a simplified proof of Rabin's Complementation Lemma for tree automata. The authors show that the Mu-Calculus is equivalent in expressive power to tree automata, which trivially implies that tree automata are closed under complementation. This equivalence is demonstrated by translating the parse tree of a Mu-Calculus formula into an alternating tree automaton, and then reducing this to a nondeterministic tree automaton. The paper also discusses how the Mu-Calculus can be used to establish the determinacy of certain infinite games, including those used in the theory of on-line algorithms. The authors provide a detailed construction for translating Mu-Calculus formulas into equivalent tree automata and prove the determinacy of infinite games with parity winning conditions. They also show that if a player has a winning strategy in a parity infinite game, then the player has a history-free winning strategy. Finally, the paper discusses the determinacy of on-line games and provides a Mu-Calculus characterization for $F_\sigma$ games, simplifying the proof of de-randomization of competitive on-line algorithms.
Reach us at info@study.space
[slides and audio] Tree Automata%2C Mu-Calculus and Determinacy (Extended Abstract)