Ampliación (ciencia informática)

En informática , especialmente en la verificación de modelos y la interpretación abstracta , el término "ampliación" se refiere al menos a dos técnicas diferentes en el análisis de sistemas de transición abstractos donde las progresiones infinitas de estados abstractos se reemplazan por un punto fijo mínimo (calculado o estimado ^{[ 1 ]} ) . El uso del término en la verificación de modelos está estrechamente relacionado con las técnicas de aceleración , reservando algunos autores la aceleración para cálculos exactos. ^{[ 2 ]}

Si bien muchos programas informáticos pueden entenderse en términos de estados y transiciones de la máquina (véase la semántica formal de los lenguajes de programación ), sus espacios de estados pueden ser demasiado grandes para representarlos y analizarlos completamente. Por lo tanto, las técnicas de análisis modernas intentan razonar sobre estados abstractos , que corresponden a muchos estados concretos.

A menudo, los estados abstractos están estructurados de tal manera que, al seguir repetidamente el efecto de los pasos del programa o al simplificar la abstracción, se obtiene una cadena de abstracciones que, como se ha demostrado, termina.

Las técnicas de ampliación y las técnicas de aceleración estrechamente relacionadas se utilizan en el análisis directo de sistemas en la disciplina de verificación de modelos simbólicos . Estas técnicas detectan ciclos, es decir, secuencias de transiciones de estados abstractos que podrían repetirse. Cuando dicha secuencia puede repetirse una y otra vez, generando nuevos estados (por ejemplo, una variable podría incrementarse en cada repetición), el análisis simbólico del programa no explorará todos estos estados en un tiempo finito. Para varias familias importantes de sistemas, como sistemas de pila , sistemas de canal o sistemas de contador , se han identificado subclases susceptibles a la llamada aceleración plana ^{[ 2 ]} para las cuales existe un procedimiento de análisis completo que calcula todo el conjunto de estados alcanzables. Este tipo de análisis directo también está relacionado con sistemas de transición bien estructurados , pero la buena estructura por sí sola no es suficiente para que dichos procedimientos sean completos (por ejemplo, el grafo de cobertura de una red de Petri siempre es finito, pero en general, sobreaproxima el espacio de estados real).

Cousot y Cousot ^{[ 3 ]} introdujeron una noción de ampliación al definir el marco de la interpretación abstracta . Un ejemplo de ampliación de un dominio abstracto que aparece en la interpretación abstracta ^{[ 4 ] [ 5 ]} sería reemplazar el límite superior de un intervalo por${\displaystyle \infty }$.