Verificación de modelos abstractos

En informática y matemáticas , la verificación de modelos abstractos es una forma de verificación de modelos para sistemas en los que desarrollar una representación real resulta demasiado complejo. Por lo tanto, el diseño se transforma en una versión "abstracta" simplificada.

El conjunto de variables se divide en visibles e invisibles según el cambio de sus valores. El espacio de estados real se resume en un conjunto más pequeño de variables visibles.

Los espacios de estados real y abstracto son conexos de 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 tomamos un elemento del espacio real, lo abstraemos y concretizamos la versión abstracta, el resultado final será un superconjunto del original.

Eso es,

${\displaystyle \eta }$(${\displaystyle \theta }$(abstracto)) = abstracto ${\displaystyle \theta }$(${\displaystyle \eta }$(real)) ${\displaystyle \supseteq }$real

• Edmund M. Clarke y Orna Grumberg y David E. Long (1994). "Verificación de modelos y abstracción". ACM Transactions on Programming Languages ​​and Systems . 16 (5): 1512– 1542. CiteSeerX 10.1.1.79.3022 . doi : 10.1145/186025.186051 . S2CID 207884170 .