Autómata Co-Büchi

En la teoría de autómatas , un autómata co-Büchi es una variante del autómata Büchi . La única diferencia es la condición de aceptación: un autómata co-Büchi acepta una palabra infinita si existe una serie, de modo que todos los estados que ocurren infinitamente a menudo en la serie estén en el conjunto de estados finales . Por el contrario, un autómata Büchi acepta una palabra si existe una serie, de modo que al menos un estado ocurre infinitamente a menudo en el conjunto de estados finales . ${\displaystyle w}$ ${\displaystyle F}$ ${\displaystyle w}$ ${\displaystyle F}$

Los autómatas Co-Büchi (deterministas) son estrictamente más débiles que los autómatas Büchi (no deterministas).

Definición formal

Formalmente, un autómata co-Büchi determinista es una tupla que consta de los siguientes componentes: ${\displaystyle {\mathcal {A}}=(Q,\Sigma ,\delta ,q_{0},F)}$

• ${\displaystyle Q}$es un conjunto finito . Los elementos de se denominan estados de . ${\displaystyle Q}$ ${\displaystyle {\mathcal {A}}}$
• ${\displaystyle \Sigma }$es un conjunto finito llamado alfabeto de . ${\displaystyle {\mathcal {A}}}$
• ${\displaystyle \delta :Q\times \Sigma \rightarrow Q}$es la función de transición de . ${\displaystyle {\mathcal {A}}}$
• ${\displaystyle q_{0}}$es un elemento de , llamado estado inicial. ${\displaystyle Q}$
• ${\displaystyle F\subseteq Q}$es el conjunto de estados final . acepta exactamente aquellas palabras con la ejecución , en las que todos los estados que ocurren infinitamente a menudo en están en . ${\displaystyle {\mathcal {A}}}$ ${\displaystyle w}$ ${\displaystyle \rho (w)}$ ${\displaystyle \rho (w)}$ ${\displaystyle F}$

En un autómata co-Büchi no determinista , la función de transición se reemplaza por una relación de transición . El estado inicial se reemplaza por un conjunto de estados iniciales . En general, el término autómata co-Büchi se refiere al autómata co-Büchi no determinista. ${\displaystyle \delta }$ ${\displaystyle \Delta }$ ${\displaystyle q_{0}}$ ${\displaystyle Q_{0}}$

Para un formalismo más completo, véase también ω-autómata .

Condición de aceptación

La condición de aceptación de un autómata co-Büchi es formalmente

${\displaystyle \exists i\forall j:\;j\geq i\quad \rho (w_{j})\in F.}$

La condición de aceptación de Büchi es el complemento de la condición de aceptación co-Büchi:

${\displaystyle \forall i\exists j:\;j\geq i\quad \rho (w_{j})\in F.}$

Propiedades

Los autómatas Co-Büchi están cerrados bajo unión, intersección, proyección y determinización.

Literatura

• Wolfgang Thomas: Autómatas en objetos infinitos. En: Jan van Leeuwen (Ed.): Manual de informática teórica. Banda B: Modelos formales y semántica. Elsevier Science Publishers ua, Ámsterdam ua 1990, ISBN  0-444-88074-7 , págs. 133-164.