Autómatas sobre objetos infinitos

Los autómatas sobre objetos infinitos leen entradas que nunca terminan, como palabras infinitas o árboles infinitos, y aceptan según los estados o transiciones que se visitan infinitamente a menudo, proporcionando la maquinaria matemática para razonar sobre sistemas continuos y no terminantes.

Definition

Un autómata omega es una máquina de estados finitos cuyas ejecuciones son infinitas, con la aceptación definida por una condición sobre el conjunto de estados visitados infinitamente a menudo; dichos autómatas reconocen conjuntos de palabras o árboles infinitos llamados lenguajes omega-regulares.

Scope

Este tema cubre los autómatas de Büchi, Muller, Rabin y de paridad sobre palabras infinitas, las condiciones de aceptación que los distinguen, los resultados de determinización y complementación, los autómatas sobre árboles infinitos y las profundas conexiones entre estos autómatas, la lógica monádica de segundo orden y los juegos infinitos utilizados en la síntesis y verificación.

Core questions

• ¿Cómo puede una máquina finita aceptar o rechazar una entrada que no tiene fin?
• ¿Por qué difieren los autómatas de Büchi no deterministas y deterministas en su poder expresivo?
• ¿Cómo se relacionan los autómatas sobre objetos infinitos con las lógicas para especificar el comportamiento del sistema?
• ¿Qué hace que la complementación de estos autómatas sea difícil y por qué es importante?

Key theories

Aceptación de Büchi y lenguajes omega-regulares

Un autómata de Büchi acepta una palabra infinita cuando algún estado de aceptación es visitado infinitamente a menudo, y los lenguajes así reconocidos, los lenguajes omega-regulares, coinciden con los definibles en lógica monádica de segundo orden sobre los números naturales.

Determinización y la condición de paridad

Los autómatas de Büchi no deterministas no pueden, en general, hacerse deterministas sin cambiar la condición de aceptación, pero la construcción de Safra los convierte en autómatas de Rabin o de paridad deterministas, lo cual es esencial para la complementación y para resolver juegos.

Clinical relevance

Los autómatas omega son la columna vertebral algorítmica de la verificación de modelos: un sistema reactivo y una propiedad de lógica temporal se traducen cada uno en autómatas sobre palabras infinitas, y la verificación de la propiedad se reduce a una prueba de vacío, lo que permite la verificación automatizada de hardware, protocolos y software concurrente.

History

Büchi introdujo los autómatas sobre palabras infinitas alrededor de 1960 para decidir la teoría monádica de segundo orden de los números naturales, McNaughton mostró cómo determinizarlos con condiciones de aceptación más fuertes, y Rabin extendió la teoría a árboles infinitos, resultados que se volvieron centrales para la verificación después de que la lógica temporal entrara en la informática a finales de la década de 1970.

Key figures

• J. Richard Büchi
• Robert McNaughton
• Michael Rabin
• Shmuel Safra

Seminal works

• thomas1990
• graedel2002

Frequently asked questions

¿Cómo puede una máquina aceptar una entrada infinita?

La aceptación se define no por alcanzar un estado final al final, ya que no hay fin, sino por los estados que se repiten. Un autómata de Büchi, por ejemplo, acepta cuando pasa por un estado de aceptación designado infinitamente a menudo durante su ejecución interminable.

¿Por qué son importantes estos autómatas para la verificación?

Los sistemas no terminantes, como los sistemas operativos y los protocolos de red, se modelan naturalmente mediante comportamientos infinitos. Propiedades como "el sistema nunca se bloquea" o "cada solicitud es finalmente atendida" se convierten en lenguajes omega-regulares, por lo que su verificación se reduce a operaciones de autómatas que un verificador de modelos puede realizar automáticamente.