Comprobación de modelo abstracto
En informática y matemáticas , la verificación de modelos de abstracción es para sistemas en los que una representación real es demasiado compleja para desarrollar el modelo solo. Entonces, el diseño se somete a una especie de traducción a una versión "abstracta" reducida.
El conjunto de variables se divide en visibles e invisibles dependiendo de su cambio de valores. El espacio inmobiliario se resume en un conjunto menor de los visibles.
Los espacios de estado real y abstracto están conectados según Galois . Esto significa que si tomamos un elemento del espacio abstracto , lo concretamos y abstraemos la versión concretada, el resultado será igual al original. Por otro lado, si elige un elemento del espacio real, lo abstrae y concreta la versión abstracta, el resultado final será un superconjunto del original.
( (abstracto)) = abstracto ( (real)) real
