A Forward-Only Construction of Semilinear Inductive Invariants for VAS

Resumen Técnico: Una Construcción de Solo Ida de Invariantes Inductivos Semilineales para VAS

Planteamiento del Problema
El problema de la alcanzabilidad para los Sistemas de Adición de Vectores (VAS), también conocidos como redes de Petri, es un problema de decisión central en la teoría de los sistemas de estado infinito. Aunque la decidibilidad fue establecida en la década de 1980 por Kosaraju y Mayer, la complejidad computacional permaneció abierta durante décadas hasta que recientemente se demostró que es de completitud Ackermann. Un enfoque alternativo significativo para la decidibilidad, introducido por Leroux, caracteriza la no-alcanzabilidad mediante invariantes inductivos semilineales. Este método se basa en un esquema de "ida y vuelta" que expande simultáneamente una sobre-aproximación hacia adelante desde la fuente y una sobre-aproximación hacia atrás desde el objetivo.

Sin embargo, este enfoque existente tiene dos limitaciones primarias:

1. Dependencia de la Simetría: La construcción depende de la simetría de los VAS, donde las ejecuciones pueden invertirse. Esta simetría se rompe en modelos asimétricos como los VAS de Ramificación (BVAS), donde las ejecuciones son de forma arbórea en lugar de secuencias lineales, lo que dificulta la extensión del método de Leroux a los BVAS.
2. Falta de Canonicidad: Los invariantes resultantes dependen equitativamente de la fuente y del objetivo. En muchos escenarios de verificación, la fuente es fija mientras que el objetivo varía; un método que produce invariantes que cambian drásticamente con el objetivo es menos canónico y más difícil de relacionar con la estructura intrínseca del sistema. Además, para subclases específicas como los VAS periódicos, el método de Leroux no garantiza que los invariantes resultantes sean periódicos.

Metodología
Los autores proponen una nueva construcción de solo ida de invariantes inductivos semilineales. A diferencia del enfoque de ida y vuelta, este método construye invariantes basándose únicamente en el conjunto de configuraciones iniciales ($C_0$) sin requerir un razonamiento hacia atrás desde el objetivo.

Los ingredientes técnicos centrales incluyen:

• VAS Periódicos: Los autores definen una clase de VAS donde el conjunto de alcanzabilidad es periódico (cerrado bajo la adición y contiene al vector cero). Demuestran que el problema de la alcanzabilidad para los VAS generales puede reducirse al problema de la alcanzabilidad para los VAS periódicos añadiendo un único contador.
• Conjuntos Casi Semilineales y Linealización: El método utiliza la caracterización geométrica de los conjuntos de alcanzabilidad de los VAS como conjuntos "casi semilineales". Estos se descomponen en conjuntos "casi lineales" ($b + P$), que luego se sobre-aproximan mediante un proceso llamado linealización ($lin(L)$).
• Vectores Interiores: Un concepto novedoso introducido en este trabajo es el de "vectores interiores" de un conjunto periódico. Estos vectores permiten al algoritmo refinar las aproximaciones empujando los vectores hacia el conjunto original, asegurando que el invariante construido permanezca disjunto del conjunto objetivo mientras mantiene la periodicidad.
• Construcción Algorítmica: El artículo presenta un algoritmo (Algoritmo 1) que refina iterativamente un conjunto periódico semilineal $Inv$. En cada iteración, identifica la diferencia entre la alcanzabilidad hacia adelante del conjunto actual y el conjunto mismo, descompone esta diferencia en componentes casi lineales y añade linealizaciones traducidas específicas a $Inv$. Se demuestra que el algoritmo termina porque la "dimensión espacial" del conjunto de diferencia disminuye estrictamente con cada iteración.

Contribuciones Clave

1. Construcción de Solo Ida: Los autores introducen un método para construir invariantes inductivos semilineales que dependen primordialmente de las configuraciones alcanzables desde la fuente. Esto produce invariantes que son más canónicos y están mejor alineados con la estructura del sistema.
2. Invariantes Periódicos para VAS Periódicos: El artículo demuestra que, para los VAS periódicos, si el conjunto de alcanzabilidad es disjunto de un conjunto semilineal objetivo, existe un invariante inductivo semilineal periódico que también es disjunto del objetivo. Esto contrasta con métodos previos que podrían producir invariantes no periódicos incluso para sistemas periódicos.
3. Reducción a VAS Periódicos: Los autores proporcionan una caracterización efectiva de los VAS periódicos y demuestran que el problema de la alcanzabilidad para los VAS simples se reduce al de los VAS periódicos. En consecuencia, los invariantes semilineales para los VAS generales pueden derivarse de los invariantes periódicos construidos para el sistema reducido.
4. Prueba de Existencia vía Oráculo: La construcción se presenta como un algoritmo con llamadas a un oráculo (para la linealización y la selección de vectores). El artículo establece la existencia de los vectores necesarios y la terminación del proceso, proporcionando una prueba constructiva de la existencia de invariantes inductivos semilineales periódicos.

Resultos

• Teorema 4.5: El conjunto de alcanzabilidad de un VAS periódico $(A, C_0)$ tiene una intersección vacía con un conjunto semilineal $C_{bad}$ si y solo si existe un invariante inductivo semilineal periódico $I$ de $(A, C_0)$ tal que $I \cap C_{bad}$ sea vacío.
• Terminación y Corrección: El algoritmo propuesto termina y devuelve un invariante inductivo periódico semilineal disjunto del conjunto objetivo, siempre que las llamadas al oráculo puedan satisfacerse. La terminación está garantizada por la disminución estricta de la dimensión espacial del conjunto $Post^*_A(Inv) \setminus Inv$ en cada paso.
• Ejemplos: El artículo ilustra el método con ejemplos donde la construcción de solo ida produce invariantes que son independientes de la configuración específica del objetivo (a diferencia del método de ida y vuelta) y, en el caso de los VAS periódicos, produce invariantes periódicos donde el método de ida y vuelta falla en hacerlo.

Significancia y Reivindicaciones
Los autores afirman que este enfoque de solo ida representa un paso hacia la extensión de las técnicas basadas en invariantes a los VAS de Ramificación (BVAS). Dado que los BVAS carecen de la simetría requerida para el razonamiento hacia atrás (las configuraciones iniciales están en las hojas, los objetivos en la raíz de los árboles de ejecución), el método de ida y vuelta dependiente de la simetría es difícil de generalizar. Al construir invariantes puramente desde la fuente, los autores sugieren que su método es más adecuado para abordar el problema abierto de la alcanzabilidad para los BVAS.

El artículo también discute la propiedad de "invariante inductivo semilineal" en el contexto de los VAS de Gramática (GVAS), conjeturando que propiedades similares pueden cumplirse, aunque esto sigue siendo un área abierta para investigaciones futuras. El trabajo se enmarca como un avance teórico en la comprensión estructural de la alcanzabilidad de los VAS, ofreciendo una herramienta más canónica para la verificación que respeta la asimetría de ciertos modelos de sistemas.