{"id":270,"date":"2015-04-23T15:52:55","date_gmt":"2015-04-23T13:52:55","guid":{"rendered":"http:\/\/duch.mimuw.edu.pl\/~bojan\/podpunkt\/?page_id=270"},"modified":"2017-10-31T13:00:39","modified_gmt":"2017-10-31T12:00:39","slug":"6-buchi-automata","status":"publish","type":"page","link":"https:\/\/www.mimuw.edu.pl\/~bojan\/20142015-2\/alg\/6-buchi-automata","title":{"rendered":"6. B\u00fcchi automata"},"content":{"rendered":"

An \"\omega\"-word is a word where positions are indexed by natural numbers. We write \"\Sigma^\omega\" for the set of \"\omega\"-words over an alphabet \"\Sigma\". To recognise languages of \"\omega\"-words, we use B\u00fcchi automata (we will later<\/a> move\u00a0a monoid style).<\/p>\n

B\u00fcchi automata.\u00a0<\/strong>A nondeterministic\u00a0B\u00fcchi automaton\u00a0<\/em>has the same syntax as a nondeterministic automaton over finite words (say, without \"\epsilon\"-transitions), i.e. it is a tuple <\/p>\n

  <\/span>   <\/span>\"\[(Q,\Sigma,I,F,\delta) \qquad \mbox{with } I,F \subseteq Q \quad \mbox{and } \delta \subseteq Q \times \Sigma \times Q\]\"<\/p>\n

where \"Q\" consisting of \u00a0states, the input alphabet, initial states, final states, and transitions. Such an automaton accepts an \"\omega\"-word if it admits some run which begins in an intial state and visits final states infinitely often. Call a language \"\omega\"-regular<\/em> if it is recognised by some nondeterministic B\u00fcchi automaton.<\/p>\n

Example.\u00a0<\/strong>The obvious question is: what about\u00a0deterministic\u00a0<\/em>B\u00fcchi automata?\u00a0<\/em>As it turns out, these are too weak. Indeed, consider the set of \"\omega\"-words over alphabet \"\set{a,b}\" where the letter \"a\" appears finitely often, this set can be described by the expression \"(a+b)^*b^\omega\". Here is a picture of a nondeterministic B\u00fcchi automaton that recognises this language:<\/p>\n

We claim that no deterministic B\u00fcchi automaton recognises this language. Suppose that there would be such an automaton. Run this automaton on the word \"ab^\omega\". Since this word contains finitely many \"a\"‘s, it should be accepted, and therefore an accepting state should be used after reading\u00a0some finite prefix \"ab^{n_1}\". Consider now the word \"ab^{n_1} a b^\omega\". Again this word should be accepted, and therefore there should be some \"n_2\" such that an accepting state is seen after reading \"ab^{n_1} a b^{n_2}\". Iterating this construction, we get an \"\omega\"-word of the form <\/p>\n

  <\/span>   <\/span>\"\[ab^{n_1} ab^{n_2} ab^{n_3} \cdots\]\"<\/p>\n

such that the automaton visits an accepting state before every \"a\", and therefore accepts, despite the word having infinitely many \"a\"‘s. Note how we crucially used determinism \u2013 by assuming that changing a suffix of the word does not change the run on a prefix. \"\Box\"<\/p>\n

\n

The automaton monoid and linked pairs<\/strong><\/p>\n

Our goal is to prove that nondeterministic B\u00fcchi automata are closed under complementation, and then a form determinisation: namely nondeterministic B\u00fcchi automata are equivalent to Boolean combinations of deterministic B\u00fcchi automata. Before proving these results, we show how to associate to each nondeterministic B\u00fcchi automaton a monoid homomorphism.<\/p>\n

The automaton homomorphism.\u00a0<\/strong>Consider\u00a0a nondeterministic B\u00fcchi automaton with states \"Q\". For a finite run \"\rho\" (i.e. a finite sequence of transitions), define the profile of the run to be the triple in \u00a0\"Q \times \set{0,1} \times Q\" such that the first coordinate is the source state, the last coordinate is the target state, and the middle coordinate says whether or not the run contains an accepting state (1 means yes). For a finite input word \"w \in \Sigma^*\", define it profile \u00a0 <\/p>\n

  <\/span>   <\/span>\"\[h(w) \subseteq Q\times \set{0,1} \times Q\]\"<\/p>\n

to be the set of all profiles of finite runs over this word. It is not difficult to see that the profile function \"h\" is compositional, and \u00a0therefore its image, call it \"M\"<\/span>, can be equipped with a monoid structure so that <\/p>\n

  <\/span>   <\/span>\"\[h : \Sigma^* \to M\]\"<\/p>\n

becomes a monoid homomorphism. This monoid homomorphism is called the\u00a0automaton\u00a0homomorphism\u00a0<\/em>associated to the automaton.<\/p>\n

Linked pairs and factorisations.\u00a0<\/b>Define a linked pair\u00a0<\/em>in the monoid \"M\" to be a pair of elements\u00a0\u00a0\"s,e \in M\" \u00a0such that \"se = s\" and \"ee=e\". This notion makes sense in any monoid, but the following notion of\u00a0accepting\u00a0<\/em>linked pair\u00a0<\/em>is specific to the monoid defined above. Define a linked pair to be accepting if there are some states \"p,q \in Q\" such that \"p\" is initial and \u00a0the elements \"s,e\", when seen as sets of triples, satisfy <\/p>\n

  <\/span>   <\/span>\"\[(p,1,q) \in s \qquad \mbox{and} \qquad (q,1,q)\]\"<\/p>\n

If a linked pair is not accepting, then it is called\u00a0rejecting.\u00a0<\/em><\/p>\n

For \"s,e \in M\" \u00a0and \"w \in \Sigma^\omega\", define an \"(s,e)\"-factorisation of \"w\" to be a factorisation\u00a0<\/p>\n

  <\/span>   <\/span>\"\[w = w_0 w_1 w_2 \cdots\]\"<\/p>\n

\u00a0into nonempty words such that \"h(w_0)=s\" and \u00a0<\/p>\n

  <\/span>   <\/span>\"\[h(w_i w_{i+1} \cdots w_j) = e \qquad \mbox{ for every }1 \le i \le j\]\"<\/p>\n

Note that the existence of such a factorisation implies that \"(s,e)\" is a linked pair.<\/p>\n

B\u00fcchi Linked Pair Lemma.\u00a0<\/strong>A word \"w \in \Sigma^\omega\" is rejected if and only if it admits an \"(s,e)\"-factorisation for some rejecting linked pair \"(s,e)\".<\/em><\/p>\n

Proof.\u00a0<\/strong>Suppose that \"w\" is rejected. Apply the Ramsey theorem, yielding some \"(s,e)\"-factorisation for some linked pair. Clearly this pair must be rejecting, since otherwise we could construct an accepting run for \"w\". For the converse implication, suppose that \"w\" admits an \"(s,e)\"-factorisation, say <\/p>\n

  <\/span>   <\/span>\"\[w = w_0 w_1 w_2 \cdots\]\"<\/p>\n

for some rejecting linked pair. Define \"x_i\" to be the position at the beginning of the word \"w_i\", in particular \"x_0\" is the first position. We claim that there cannot be any accepting run on \"w\". Toward a contradiction, suppose that \"w\" does admit an accepting run, call it \"\rho\". If \"\rho\" is accepting, then by the pigeonhole principle one can find some \"0 < i < j\" such that accepting states are seen between \"x_i\" and \"x_j\", and the same state, call it \"q\", is seen in positions \"x_i\" and \"x_j\". This means that there is some\u00a0initial state \"p\" that the word \"w_0 \cdots w_{j-1}\" admits a run of profile \"(p,1,q)\". In other words, we have <\/p>\n

  <\/span>   <\/span>\"\[(p,1,q) \in h(w_0 \cdots w_{j-1}) = s\]\"<\/p>\n

By the same kind of reasoning, we conclude that <\/p>\n

  <\/span>   <\/span>\"\[(q,1,q) \in h(w_i \cdots w_{j-1})=e\]\"<\/p>\n

and therefore the linked pair \"(s,e)\" is accepting, contradicting our assumption. \"\Box\"<\/p>\n

 <\/p>\n

\n

 <\/p>\n

Complementation of B\u00fcchi automata<\/strong><\/p>\n

As an application of the automaton homomorphism, we prove that languages recognised by nondeterministic B\u00fcchi automata are closed under complementation. This is B\u00fcchi’s original proof of the result. We will also use the same ideas to prove determinisation, which is done here.<\/a><\/p>\n

Theorem.\u00a0<\/strong>For every nondeterministic B\u00fcchi automaton, the complement of its language is recognised by a nondeterministic\u00a0B\u00fcchi\u00a0automaton<\/em>.<\/p>\n

Proof.\u00a0<\/strong>Consider a language \"L \subseteq \Sigma^\omega\" recognised by a nondeterministic B\u00fcchi automaton, and let \"h : \Sigma^* \to M\" be the automaton homomorphism corresponding to this automaton.\u00a0By the B\u00fcchi Linked Pair Lemma, the complement of \"L\" is equal to <\/p>\n

  <\/span>   <\/span>\"\[\bigcup_{(s,e)} h^{-1}(s) (h^{-1}(e))^\omega\]\"<\/p>\n

with the union ranging over rejecting linked pairs. The above language is easily seen to be recognised by a nondeterministic B\u00fcchi automaton. \"\Box\"<\/p>\n","protected":false},"excerpt":{"rendered":"

An -word is a word where positions are indexed by natural numbers. We write for the set of -words over an alphabet . To recognise languages of -words, we use B\u00fcchi automata (we will later move\u00a0a monoid style). B\u00fcchi automata.\u00a0A nondeterministic\u00a0B\u00fcchi automaton\u00a0has the same syntax as a nondeterministic automaton over finite words (say, without -transitions), […]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":42,"menu_order":0,"comment_status":"open","ping_status":"open","template":"","meta":{"_acf_changed":false,"inline_featured_image":false,"footnotes":""},"class_list":["post-270","page","type-page","status-publish","hentry"],"acf":[],"_links":{"self":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/270"}],"collection":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/comments?post=270"}],"version-history":[{"count":22,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/270\/revisions"}],"predecessor-version":[{"id":296,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/270\/revisions\/296"}],"up":[{"embeddable":true,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/42"}],"wp:attachment":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/media?parent=270"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}