💻 computer science

Kofola 1.0: A Modular Approach to {\omega}-Regular Complementation and Inclusion Checking (Technical Report)

Este artículo presenta Kofola, una herramienta eficiente y robusta que emplea un marco modular para descomponer autómatas de Büchi en componentes fuertemente conexos para la comprobación de complemento e inclusión adaptada, demostrando un rendimiento superior a las herramientas más avanzadas mediante la comprobación de vaciedad al vuelo y nuevas heurísticas.

Autores originales: Ondrej Alexaj, Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, Yong Li, Nicolas Mazzocchi

Publicado 2026-05-18

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Ondrej Alexaj, Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, Yong Li, Nicolas Mazzocchi

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que eres un inspector de control de calidad para una fábrica masiva e infinita. Esta fábrica produce flujos interminables de productos (llamados "palabras" en informática). Tienes dos máquinas: Máquina A y Máquina B.

Tu trabajo es responder una pregunta muy difícil: "¿Cada producto individual que produce la Máquina A también es producido por la Máquina B?"

Si la respuesta es "Sí", entonces la Máquina A es segura para usar. Si hay incluso un producto que la Máquina A produce y la Máquina B nunca produce, entonces la Máquina A es insegura.

Este es el problema central de la Verificación de Inclusión de Lenguajes. Es una tarea fundamental para verificar que el software y el hardware informáticos se comporten correctamente. Sin embargo, debido a que los flujos de productos son infinitos, verificar esto manualmente es imposible. Necesitas un robot superinteligente para hacerlo.

Aquí entra Kofola, un robot nuevo y altamente eficiente diseñado para resolver este problema. Así es como funciona, desglosado en conceptos simples:

1. La Vieja Forma vs. La Forma Kofola

Anteriormente, los robots que intentaban resolver esto tenían que observar toda la planta de la fábrica a la vez. Intentaban construir un mapa gigante de cada posible ruta que la Máquina A podría tomar y compararlo con la Máquina B. Este mapa era tan enorme que a menudo hacía explotar el cerebro del robot (un problema llamado "explosión del espacio de estados").

El Secreto de Kofola: El Enfoque Modular
En lugar de observar toda la fábrica a la vez, Kofola es un maestro organizador. Observa la Máquina B y dice: "Esta fábrica no es un gran desorden; en realidad está hecha de barrios distintos".

Kofola descompone la Máquina B en Componentes Fuertemente Conectados (CFC). Piensa en estos como diferentes habitaciones o zonas de la fábrica:

Los Cul-de-sac: Habitaciones donde la máquina deja de producir productos.
Los Bucles Simples: Habitaciones donde la máquina gira en círculos haciendo lo mismo una y otra vez.
Las Zonas Deterministas: Habitaciones donde la máquina tiene solo una opción en cada paso (como un tren en una vía única).
Las Zonas Caóticas: Habitaciones donde la máquina tiene muchas opciones y puede ir en diferentes direcciones (como un laberinto).

Kofola trata cada "barrio" de manera diferente. Utiliza una herramienta especializada y simple para los bucles simples y una herramienta pesada para las zonas caóticas. No desperdicia energía intentando resolver las partes fáciles con un martillo neumático.

2. El Nuevo Descubrimiento "IADAC"

El artículo introduce un nuevo tipo de barrio llamado IADAC (Componente Aceptador Casi Determinista Inicial).

La Analogía: Imagina un pasillo que conduce a una habitación. El pasillo es una vía recta de un solo carril (determinista). Una vez que entras en la habitación, podrías tener opciones. Pero aquí está el truco: una vez que sales de esa habitación, nunca puedes volver al pasillo.
Por qué importa: Como el pasillo es tan predecible, Kofola puede usar un método muy rápido y ligero para verificarlo, en lugar del método pesado y lento necesario para las partes caóticas. Este es un nuevo tipo de zona que los autores identificaron y optimizaron.

3. El Inspector "Perezoso" (Verificación al vuelo)

Por lo general, para verificar si la fábrica es segura, tienes que construir el mapa completo de la fábrica antes de poder decir "Seguro" o "Inseguro".

Kofola es máximamente perezoso (en el buen sentido). Comienza a construir el mapa, pero tan pronto como encuentra evidencia suficiente para decidir la respuesta, se detiene.

Si encuentra un "producto malo" al principio, inmediatamente grita: "¡Inseguro!" y deja de trabajar.
No pierde tiempo mapeando el resto de la fábrica si la respuesta ya está clara.

Esto se hace utilizando un nuevo algoritmo de "verificación de vacuidad". Imagina que buscas un tipo específico de error en una habitación oscura. En lugar de encender las luces de toda la habitación, solo diriges tu linterna por el camino que estás recorriendo. Si encuentras el error, te detienes. Si recorres todo el camino y no lo encuentras, sabes que la habitación está libre. Kofola hace esto instantáneamente mientras construye el mapa.

4. Los Resultados: Kofola Gana la Carrera

Los autores probaron a Kofola contra los mejores robots existentes (herramientas como Spot, Rabit y Bait) utilizando miles de planos de fábricas del mundo real.

Robustez: Kofola fue la única herramienta que resolvió con éxito cada caso de prueba individual sin fallar ni quedarse sin memoria. Las demás fallaron en muchas de las más difíciles.
Velocidad: En muchos problemas prácticos, Kofola no fue solo más rápido; fue órdenes de magnitud más rápido. En algunos casos, mientras otras herramientas aún intentaban construir el mapa después de 2 minutos, Kofola ya había terminado en una fracción de segundo.
Tamaño: Los mapas que Kofola construyó fueron a menudo mucho más pequeños y compactos que los construidos por la competencia.

Resumen

Kofola es una nueva herramienta supereficiente para verificar si un sistema informático está "contenido" dentro de otro. Funciona mediante:

Descomponer el problema en barrios más pequeños y manejables.
Usar la herramienta correcta para cada tipo de barrio específico (incluyendo un nuevo tipo que descubrió).
Ser perezoso, deteniendo el trabajo en el momento en que tiene suficiente información para dar una respuesta.

El resultado es una herramienta que es más rápida, más confiable y maneja problemas mucho más grandes y complejos que cualquier otra disponible actualmente. Es una mejora significativa para el "control de calidad" de los sistemas informáticos.

Resumen Técnico: Kofola 1.0 – Un Enfoque Modular para la Complementación ω-Regular y la Verificación de Inclusión

Enunciado del Problema

La verificación de inclusión de lenguajes para autómatas de Büchi (AB) es un problema fundamental en la verificación basada en teoría de autómatas, con aplicaciones críticas en la verificación de modelos, la monitorización y la demostración de teoremas. El problema es completo en PSpace y sigue siendo computacionalmente exigente a medida que las especificaciones del sistema crecen en tamaño y complejidad. Decidir si $L_1 \subseteq L_2$ se reduce a verificar la vacuidad de $L_1 \cap \overline{L_2}$ , donde $\overline{L_2}$ es el complemento de $L_2$ . Esta reducción presenta dos desafíos principales:

Complementación Compacta: Construir el autómata complemento $\overline{L_2}$ de manera eficiente sin provocar una explosión del espacio de estados.
Exploración Eficiente: Explorar el autómata producto de $L_1 \cap \overline{L_2}$ , que a menudo es enorme.

Las herramientas existentes dependen en gran medida de construcciones de complementación basadas en Ramsey o en determinización clásicas, que datan de hace más de tres décadas. Aunque existen avances recientes en complementación, no se han integrado completamente en verificadores de inclusión prácticos.

Metodología

El artículo presenta Kofola, una herramienta eficiente implementada en C++ que aplica un marco de complementación modular de última generación. La metodología se basa en descomponer el autómata de entrada en componentes fuertemente conexos (CFC) y aplicar algoritmos de complementación adaptados a cada componente según sus propiedades estructurales.

1. Descomposición Estructural y Clasificación de Componentes

Kofola realiza un análisis estructural detallado del autómata a complementar ( $A_2$ ). Clasifica sus CFC maximales en cuatro categorías distintas:

Componentes no aceptantes: Se gestionan mediante la construcción de subconjuntos tradicional.
Componentes Aceptantes Intrínsecamente Débiles (IWAC): Componentes donde todos los ciclos aceptan.
Componentes Aceptantes Deterministas (DAC): Componentes con transiciones únicamente deterministas.
Componentes Aceptantes Casi Deterministas Iniciales (IADAC): Un nuevo tipo de componente identificado en este artículo. Son CFC deterministas alcanzables desde estados iniciales mediante CFC deterministas, permitiendo no determinismo solo en caminos sin ciclos entre CFC.
Componentes Aceptantes No Deterministas (NAC): Los CFC aceptantes restantes.

2. Marco de Complementación Modular

Para cada tipo de componente, Kofola aplica un algoritmo de complementación parcial dedicado:

IWAC: Utiliza la construcción clásica de Miyano-Hayashi, generando una condición de aceptación $Inf(1)$.
DAC: Utiliza una modificación del algoritmo NCSB, generando una condición de aceptación $Inf(2)$.
NAC: Soporta dos enfoques dependiendo de la tarea:
- Complementación: Utiliza un enfoque basado en determinización (variante de Safra-Piterman) para producir autómatas más pequeños.
- Verificación de Inclusión: Utiliza un enfoque basado en rebanadas (slice-based), que es más adecuado para la prueba de vacuidad del producto en tiempo de ejecución.
IADAC: El artículo introduce un nuevo algoritmo parcial para estos componentes. Determiniza los IADAC mediante una construcción de subconjuntos y emite una marca de rechazo ($Fin(0)$) siempre que una ejecución rastreada observe una transición aceptante. La corrección se basa en el hecho de que las ejecuciones en IADAC están acotadas debido a su no determinismo restringido.

El algoritmo de nivel superior sincroniza estas construcciones parciales. El autómata complemento resultante es un Autómata de Rabin Generalizado Simple (SGRA) con una única condición de aceptación de la forma $Fin(0) \land Inf(1) \land \dots \land Inf(k-1)$ .

3. Verificación de Vacuidad en Tiempo de Ejecución

Para abordar la explosión del espacio de estados en la verificación de inclusión, Kofola emplea un nuevo algoritmo de verificación de vacuidad en tiempo de ejecución para el SGRA resultante.

Construcción Perezosa: A diferencia de las herramientas que requieren la construcción explícita del autómata producto completo, Kofola explora el espacio de estados de manera perezosa.
Algoritmo: El algoritmo es una variante del algoritmo de Couvreur extendida con un predicado $Fin$. Realiza una búsqueda en profundidad, gestionando una pila de conjuntos de transiciones para detectar CFC.
Terminación: La búsqueda termina tan pronto como el espacio de estados explorado es suficiente para decidir el resultado (ya sea encontrando un ciclo aceptante o probando la vacuidad). Esto minimiza la parte generada del complemento, lo cual es crucial ya que la complementación es la fuente principal de explosión.

Contribuciones Clave

Herramienta Kofola: Una herramienta eficiente y modular para la complementación de AB y la verificación de inclusión de lenguajes.
Identificación de IADAC: La introducción y formalización de los Componentes Aceptantes Casi Deterministas Iniciales (IADAC) como una clase estructural distinta.
Nuevo Algoritmo de Complementación: Un algoritmo parcial dedicado para IADAC que genera la condición $Fin(0)$, permitiendo la construcción de un único par de Rabin generalizado.
Verificación de Vacuidad Perezosa: Un nuevo algoritmo en tiempo de ejecución para SGRAs que evita la construcción explícita del autómata completo, permitiendo una terminación temprana.
Marco Modular: Una arquitectura flexible que permite combinar diferentes algoritmos parciales de manera sincrónica basándose en el análisis estructural.

Resultados Experimentales

Los autores evaluaron Kofola frente a herramientas de última generación: Spot, Ranker, Owl, Bait, Forklift y Rabit.

Pruebas de Referencia de Complementación

Conjunto de Datos: 31.273 autómatas de diversas fuentes (terminación de programas, lógica de palabras de Sturmian, hiperpropiedades, S1S, traducción LTL y generación aleatoria).
Robustez: Kofola fue la única herramienta que complementó con éxito los 31.273 autómatas de entrada. La herramienta más robusta siguiente, Spot, falló en 2 instancias debido a límites de memoria.
Tamaño: Kofola produjo autómatas complemento significativamente más pequeños en promedio (79,24 estados) en comparación con Spot (115,38 estados) y Ranker (45,80 estados, aunque Ranker falló en 443 instancias).
Rendimiento: Kofola resolvió la mayor cantidad de instancias y a menudo superó a los competidores en varias órdenes de magnitud en tiempo de ejecución.

Pruebas de Referencia de Verificación de Inclusión

Conjunto de Datos: 1.014 problemas de inclusión derivados de la terminación de programas, la verificación de sistemas concurrentes, la verificación de modelos de hiperpropiedades y la demostración de teoremas.
Rendimiento: Kofola resolvió la mayor cantidad de instancias (solo 2 sin resolver) y tuvo el tiempo de ejecución total más bajo (141 segundos para problemas resueltos).
Comparación: Kofola ganó estrictamente a Spot(Det) en 263 instancias y perdió en solo 0. Superó significativamente a las herramientas basadas en Ramsey (Bait, Forklift, Rabit), que a menudo requirieron un orden de magnitud más de tiempo.
Observación: El 98% de los autómatas en el lado derecho de las consultas de inclusión (aquellos que se complementan) eran autómatas tipo ascensor (que no contienen NAC), destacando la relevancia práctica de explotar las propiedades estructurales.

Significado y Afirmaciones

El artículo afirma que Kofola establece un nuevo estándar de eficiencia y robustez en la complementación de AB y la verificación de inclusión. Su importancia radica en:

Practicidad: Trae técnicas modernas de complementación basadas en descomposición a la verificación de inclusión práctica, superando las construcciones clásicas.
Escalabilidad: Al combinar la descomposición estructural con la verificación de vacuidad perezosa en tiempo de ejecución, mitiga eficazmente la explosión del espacio de estados, resolviendo instancias que son intratables para las herramientas existentes.
Extensibilidad: La arquitectura modular permite la integración de nuevos algoritmos de complementación parcial para tipos específicos de componentes.

Los autores posicionan a Kofola no meramente como una mejora incremental, sino como una herramienta altamente competitiva que a menudo supera a las soluciones de última generación en varias órdenes de magnitud en pruebas de referencia derivadas de aplicaciones prácticas.