A Büchi automaton is the extension of a finite state automaton to infinite inputs. It accepts an infinite input sequence iff there exists a run of the automaton (in case of a deterministic automaton, there is exactly one possible run) which visits (at least) one of the final states infinitely often. It is named after the Swiss mathematician Julius Richard Büchi who invented this kind of automaton in 1962.

PropertyValue
dbpprop:abstract
  • A Büchi automaton is the extension of a finite state automaton to infinite inputs. It accepts an infinite input sequence iff there exists a run of the automaton (in case of a deterministic automaton, there is exactly one possible run) which visits (at least) one of the final states infinitely often. It is named after the Swiss mathematician Julius Richard Büchi who invented this kind of automaton in 1962. Automata on infinite words are useful for specifying behavior of nonterminating systems, such as hardware or operating systems. For such systems, you may want to specify a property such as "for every request, an acknowledge eventually follows", or its negation "there is a request which is not followed by an acknowledge". The latter is a property of infinite words: you cannot say of a finite sequence that it satisfies this property. Büchi automata recognize the omega-regular languages, the infinite word version of regular languages. A language defined by a Rabin automaton, Streett automaton, parity automaton, or Muller automaton is also omega-regular. These automata have more powerful acceptance conditions, and are therefore often more succinct (use fewer states to express the same language).
  • Der Büchi-Automat (nach dem Schweizer Mathematiker Julius Richard Büchi) ist eine spezielle Form des ω-Automaten. Dieser Automatentyp kann benutzt werden, um sowohl Sprachen über unendliche Wörter als auch über unendliche Bäume zu erkennen.
  • Un automate de Büchi est un automate fini avec une condition d'acceptation particulière : une trace est acceptée si et seulement si elle passe un nombre infini de fois par au moins un état acceptant. Les automates de Büchi déterministes et non déterministes ne sont pas équivalents. Par contre, tout automate de Büchi est équivalent à un automate de Rabin déterministe. Les automates de Büchi non déterministes représentent exactement les propriétés de la logique monadique de second ordre à un successeur (S1S), dites aussi propriétés ω-régulières. La logique S1S est strictement plus expressive que la logique temporelle linéaire.
  • Automat Büchiego to rozszerzenie automatu skończonego na słowa nieskończone. Automat Büchiego składa się z: alfabetu zbioru stanów z wyróżnionym stanem startowym oraz podzbiorem stanów akceptujących funkcji przejścia, która pobiera aktualny stan oraz literę alfabetu i zwraca nowy stan (deterministyczne automaty Büchiego), lub relacji przejścia, która może zwracać wiele stanów (niedeterministyczne automaty Büchiego) Słowo (nieskończone) jest akceptowane przez automat Büchiego, jeśli stan akceptujący wystąpi w tym słowie nieskończenie wiele razy. W przeciwieństwie do zwykłych automatów skończonych, gdzie automaty deterministyczne i niedeterministyczne miały taką samą moc, niedeterministyczne automaty Büchiego są silniejsze od deterministycznych. Niedeterministyczne automaty Büchiego są zamknięte ze względu na dopełnienie, przecięcie i alternatywę. Dopełnienie automatu deterministycznego może być automatem niedeterministycznym.
dbpprop:hasPhotoCollection
dbpprop:reference
rdf:type
rdfs:comment
  • A Büchi automaton is the extension of a finite state automaton to infinite inputs. It accepts an infinite input sequence iff there exists a run of the automaton (in case of a deterministic automaton, there is exactly one possible run) which visits (at least) one of the final states infinitely often. It is named after the Swiss mathematician Julius Richard Büchi who invented this kind of automaton in 1962.
  • Der Büchi-Automat (nach dem Schweizer Mathematiker Julius Richard Büchi) ist eine spezielle Form des ω-Automaten. Dieser Automatentyp kann benutzt werden, um sowohl Sprachen über unendliche Wörter als auch über unendliche Bäume zu erkennen.
  • Un automate de Büchi est un automate fini avec une condition d'acceptation particulière : une trace est acceptée si et seulement si elle passe un nombre infini de fois par au moins un état acceptant. Les automates de Büchi déterministes et non déterministes ne sont pas équivalents. Par contre, tout automate de Büchi est équivalent à un automate de Rabin déterministe.
  • Automat Büchiego to rozszerzenie automatu skończonego na słowa nieskończone.
rdfs:label
  • Büchi automaton
  • Büchi-Automat
  • Automate de Büchi
  • Automat Büchiego
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of
is owl:sameAs of