Automate de Büchi
Un article de Wikipédia, l'encyclopédie libre.
 |
Cet article est une ébauche concernant l’informatique.
Vous pouvez partager vos connaissances en l’améliorant. (Comment ?).
|
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 les états acceptants.
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 LTL, dites aussi propriétés ω-régulières.
[modifier] Références
- Wolfgang Thomas, Automata on infinite objects, dans Handbook of Theoretical Computer Science : Formal Models and Semantics, tome B (Jan Van Leeuwen, éd.), MIT Press, ISBN 0-262-72015-9
