{"id":289,"date":"2015-04-23T16:28:41","date_gmt":"2015-04-23T14:28:41","guid":{"rendered":"http:\/\/duch.mimuw.edu.pl\/~bojan\/podpunkt\/?page_id=289"},"modified":"2015-04-23T16:28:41","modified_gmt":"2015-04-23T14:28:41","slug":"determinisation","status":"publish","type":"page","link":"https:\/\/www.mimuw.edu.pl\/~bojan\/20142015-2\/alg\/6-buchi-automata\/determinisation","title":{"rendered":"Determinisation"},"content":{"rendered":"

As we showed in the example of “finitely many \"a\"‘s”, deterministic B\u00fcchi automata are not closed under complement. However, if we simply add complementation, i.e. we close them under Boolean combinations, then we get a (deterministic) model that is equivalent to nondeterministic B\u00fcchi automata.<\/p>\n

McNaughton’s Theorem.\u00a0<\/strong>For every nondeterministic B\u00fcchi automaton, its language is a Boolean combination of languages recognised by deterministic B\u00fcchi automata<\/em>.<\/p>\n

This theorem was originally proved by McNaughton. The construction below is slightly similar to the original one, and different from the more often used constructions that do not use algebra, e.g. the Safra construction or the Muller-Schupp construction. The key concept in the proof is the idea of a\u00a0tail \"\Jj\"-class.\u00a0<\/em><\/p>\n

Tail \"\Jj\"-class.\u00a0<\/b>For a word \"w \in \Sigma^\omega\", we say that \"m \in M\" <\/span>appears<\/em>\u00a0<\/span>arbitrarily far\u00a0<\/em>if there are infinitely many positions \"x\" such that for some \"y\" (depending on \"x\") the infix from \"x\" to \"y\" has type \"m\".\u00a0<\/span>It is easy to see if \"m,n \in M\" appear arbitrarily far, then there is some \"k \in M\" that also appears arbitrarily far, and is \"\Jj\"-heavier or equivalent to both of them. Therefore there is a unique heaviest \"\Jj\"-class that contains elements which appear arbitrarily far, call this \"\Jj\"-class the <\/span>tail \"\Jj\"-class\u00a0<\/em>of the word.<\/span><\/p>\n

Lemma.\u00a0<\/strong>For every \"\Jj\"-class, the set of \"\omega\"-words with this tail \"\Jj\"-class is a Boolean combination of languages recognised by deterministic B\u00fcchi automata<\/em>.<\/p>\n

Proof.\u00a0<\/strong>For every \"m \in M\" there is a deterministic B\u00fcchi automaton which recognises words where \"m\" appears arbitrarily far. The automaton works like this: it enters an accepting state whenever it sees a word that contains \"m\" as an infix. Then it returns to the initial state, and restarts the process, and so on forever. The automaton for the tail \"\Jj\"-class is a Boolean combination of these automata. \"\Box\"<\/p>\n

Recall that B\u00fcchi’s Linked Pair Lemma said that acceptance or rejection by a nondeterministic B\u00fcchi automaton is uniquely determined by the existence of linked pair factorisations. Therefore, McNaughton’s theorem will follow from the lemma bellow, which shows how to use deterministic automata to see if there exist linked pair factorisations.<\/p>\n

Lemma.\u00a0<\/strong>For every linked pair \"(s,e)\" in the monoid \"M\" the set of words which admit an \"(s,e)\"-factorisation is a Boolean combination of languages recognised by deterministic B\u00fcchi automata<\/em>.<\/p>\n

Proof. <\/strong>For a word \"w \in \Sigma^\omega\", we say that the pair \"(s,e,e)\" appears\u00a0arbitrarily far\u00a0<\/em>if there are infinitely many positions \"x\" such that for some \"y < z\" (depending on \"x\") the prefix up to \"x\" has type \"s\", \u00a0the infix from \"x\" to \"y\" has type \"e\", and the infix from \"y\" to \"z\" also has type \"e\". Using the same idea as before, one can show that the set of words where \"(s,e)\" appears arbitrarily far is a Boolean combination of languages recognised by deterministic B\u00fcchi automata. Therefore, to \u00a0complete the lemma it suffices to show that a word admits\u00a0an \"(s,e)\"-factorisation if and only if \"(s,e,e)\" appears arbitrarily far, and the \"\Jj\"-class of contains \"e\". The left-to-right implication is immediate, so let us do the right-to-left implication.<\/p>\n

Suppose then that the tail \"\Jj\"-class of \"w\" contains \"e\", and that \"(s,e,e)\" appears arbitrarily far to the right. Since \"(s,e,e)\" appears arbitrarily far to the right, there exists a factorisation <\/p>\n

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

such that every nonempty prefix \"w_0 \cdots w_i\" has type \"s\" and every \"w_i\" has both a prefix and suffix of type \"e\". \u00a0Since the tail \"\Jj\"-class contains \"e\", it follows that for all but finitely many \"i\", the type of \"w_i\" is \"\Jj\"-equivalent to \"e\". Without loss of generality, we assume that every \"w_i\" has type that is \"\Jj\"-equivalent to \"e\". Since this type begins with \"e\", ends with \"e\", and is \"\Jj\"-equivalent to \"e\", it must be in the \"\Hh\"-class of \"e\" by the Eggbox Lemma. Furthermore, this \"\Hh\"-class, call it \"H\", is a group, because it contains an idempotent. By grouping the decomposition, we can assume without loss of generality that there is some \"h \in H\" such that every word \"w_1 \cdots w_i\" has type \"h\". This implies that every \"w_i\" has type that is the identity in the group, which is the idempotent \"e\". \"\Box\"<\/p>\n","protected":false},"excerpt":{"rendered":"

As we showed in the example of “finitely many ‘s”, deterministic B\u00fcchi automata are not closed under complement. However, if we simply add complementation, i.e. we close them under Boolean combinations, then we get a (deterministic) model that is equivalent to nondeterministic B\u00fcchi automata. McNaughton’s Theorem.\u00a0For every nondeterministic B\u00fcchi automaton, its language is a Boolean […]<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":270,"menu_order":0,"comment_status":"open","ping_status":"open","template":"","meta":{"_acf_changed":false,"inline_featured_image":false,"footnotes":""},"class_list":["post-289","page","type-page","status-publish","hentry"],"acf":[],"_links":{"self":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/289"}],"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=289"}],"version-history":[{"count":6,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/289\/revisions"}],"predecessor-version":[{"id":295,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/289\/revisions\/295"}],"up":[{"embeddable":true,"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/pages\/270"}],"wp:attachment":[{"href":"https:\/\/www.mimuw.edu.pl\/~bojan\/wp-json\/wp\/v2\/media?parent=289"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}