Ampliación (informática)
En ciencias de la computación , especialmente la verificación de modelos y la interpretación abstracta , la 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 adivinado [1] ) . El uso del término en la verificación de modelos está estrechamente relacionado con las técnicas de aceleración , algunos autores reservan la aceleración para cálculos exactos. [2]
Si bien muchos programas de computadora pueden entenderse en términos de estados y transiciones de la máquina (consulte la semántica formal de los lenguajes de programación ), sus espacios de estado pueden ser demasiado grandes para representarlos y analizarlos por completo. Por lo tanto, las técnicas modernas de análisis 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 se ha comprobado que 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 . Las técnicas detectan ciclos, es decir, secuencias de transiciones de estado abstracto que podrían repetirse. Cuando tal secuencia puede repetirse una y otra vez, generando nuevos estados (por ejemplo, una variable puede 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 los sistemas pushdown, los sistemas de canales o los sistemas de contador , se han identificado subclases susceptibles de la denominada aceleración plana .[2] para el cual 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 estructuración por sí sola no es suficiente para que tales procedimientos estén completos (por ejemplo, el gráfico de cobertura de una red de Petri siempre es finito pero, en general, se aproxima en exceso al verdadero espacio de Estados).
Cousot y Cousot [3] han introducido 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 .
