AGV 10.1 -- The Muller Acceptance Condition

Previous chapter: The Emerson-Lei algorithm

This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner

Introdcution

We already established that while the languages that can be recognized with nondeterministic Büchi automata are exactly the $\omega$-regular languages, the languages that can be recognized with deterministic Büchi automata are a strictly smaller set.

We now repair this deficiency with a more expressive acceptance condition, the Muller condition. McNaughton’s theorem states that the set of languages recognizable by deterministic Muller automata are again exactly the $\omega$-regular languages.

We will see later that it is very useful to have a deterministic automaton for a given $\omega$-language, for example in synthesis, where we construct the game between the system and the environment from a deterministic automaton that recognizes the winning plays for the system player.

Since the complementation of deterministic Muller automata is a very simple operation, McNaughton’s theorem also provides an alternative proof for the result of Section 5 that the $\omega$-regular languages are closed under complementation.

Muller Acceptance Condition

$\textbf{Definition 10.1. } \text{The }\textit{Muller Acceptance Condition }\small\text{MULLER} \normalsize(\mathcal{F})\text{ on a set of sets of states }\newline\mathcal{F}\subseteq 2^Q\text{ is the set}$

$$\small\text{MULLER}\normalsize(\mathcal{F})=\lbrace\alpha\in Q^\omega\mid\text{Inf}(\alpha)\in\mathcal{F}\rbrace$$

$\text{An automaton }\mathcal{A} = (\Sigma,Q,I,T,Acc) \text{ with }Acc = \small\text{MULLER} \normalsize(\mathcal{F})\text{ is called a }\textit{Muller Automaton.}\newline\text{The set }\mathcal{F}\text{ is called the set of }\textit{accepting subsets }(\text{or the }\textit{table})\text{ of }\mathcal{A}.$

Let’s do a small recap from section 2.3:

• Büchi Condition

  • $\small\text{BÜCHI} \normalsize(F) = \lbrace\alpha\in Q^\omega \mid \text{Inf}(\alpha) \cap F \neq \varnothing\rbrace$
  • word $\alpha$ visit some state in set $F$ infinitely often.

• Muller Acceptance Condition

  • $\small\text{MULLER}\normalsize(\mathcal{F})$
  • word $\alpha$ visit some set of states in set $\mathcal{F}$ infinitely often.

We can see Muller Acceptance Condition are more expressive in terms of visiting accepting states, because you can require the word to visit a set of states infinitely often instead just one state out of the whole set.

Example

Consider the deterministic automaton over the alphabet $\Sigma=\lbrace a, b\rbrace$ shown below.

For the table $\mathcal{F}=\lbrace\lbrace q\rbrace\rbrace$, it means the automaton can only visit $\lbrace q\rbrace$ infinitely often. We obtain the Muller automaton $\mathcal{A}$ recognizing the language $\mathcal{L(A)}=(a+b)^\ast b^\omega$;

For the table $\mathcal{F}’=\lbrace\lbrace q\rbrace\lbrace p,q\rbrace\rbrace$, it means the automaton has to visit either $\lbrace q\rbrace$ or $\lbrace p,q\rbrace$ infinitely often. We obtain the Muller automaton $\mathcal{A’}$ recognizing $\mathcal{L(A’)}=(a^\ast b)^\omega$.

Summary

We introduced Muller Acceptance Condition, which is slightly more advanced than the Büchi Acceptance Condition:

Aspect	Büchi Acceptance	Muller Acceptance
Acceptance states	At least one accepting state must appear infinitely often.	The set of states that visited infinitely often must match a subset in $\mathcal{F}$
Condition Set	$F$ is the set of accepting states	$\mathcal{F}$ is the set of the set of accepting states (subset of the set)
Expressiveness	Less expressive (example)	Fully expressive
Complexity	Simpler and easier to implement.	More complex, requires tracking recurring state sets.

In the following sections, we will discuss about the translation from Büchi automata to Muller automata.

---

Next chapter: From Büchi automata to Muller automata

Further Reading: