Matriz ligada a la diferencia

En la verificación de modelos , un campo de la informática , una matriz ligada de diferencia (DBM) es una estructura de datos utilizada para representar algunos politopos convexos llamados zonas . Esta estructura se puede usar para implementar de manera eficiente algunas operaciones geométricas sobre zonas, como probar el vacío, la inclusión, la igualdad y calcular la intersección y la suma de dos zonas. Se utiliza, por ejemplo, en el comprobador de modelos de Uppaal ; donde también se distribuye como biblioteca independiente. ^[1]

Más precisamente, existe una noción de DBM canónico; existe una relación de uno a uno entre los DBM canónicos y las zonas, y de cada DBM se puede calcular eficientemente un DBM equivalente canónico. Por lo tanto, la igualdad de zona se puede probar comprobando la igualdad de los DBM canónicos.

Se utiliza una matriz ligada a diferencias para representar algún tipo de politopos convexos. Esos politopos se llaman zona . Ahora están definidos. Formalmente, una zona se define mediante ecuaciones de la forma , y , con algunas variables y una constante.${\ estilo de visualización x \ leq c}$${\ estilo de visualización x \ geq c}$${\displaystyle x_{1}\leq x_{2}+c}$${\displaystyle x_{1}\geq x_{2}+c}$${\ estilo de visualización x_ {1}}$${\ estilo de visualización x_ {2}}$${\ estilo de visualización c}$

Las zonas originalmente se llamaban región , ^[2] pero hoy en día este nombre generalmente denota región , un tipo especial de zona. Intuitivamente, una región puede considerarse como una zona mínima no vacía, en la que las constantes utilizadas en la restricción están acotadas.

Dadas las variables, existen exactamente diferentes restricciones no redundantes posibles, restricciones que usan una sola variable y un límite superior, restricciones que usan una sola variable y un límite inferior, y para cada uno de los pares ordenados de variable , un límite superior en . Sin embargo, un politopo convexo arbitrario puede requerir un número arbitrariamente grande de restricciones . Incluso cuando , puede haber un gran número arbitrario de restricciones no redundantes para algunas constantes. Esta es la razón por la que los DBM no se pueden extender de zonas a politopos convexos.${\ estilo de visualización n}$${\ estilo de visualización n (n + 1)}$${\ estilo de visualización n}$${\ estilo de visualización n}$${\ estilo de visualización n^{2}}$${\ estilo de visualización (x, y)}$${\ estilo de visualización xy}$${\displaystyle \mathbb {R} ^{n}}$${\displaystyle n=2}$${\displaystyle (x<iy+c_{i})_{i\in \mathbb {N} }}$${\displaystyle c_{i}}$

Figura en la que se muestra , que son disjuntos${\textstyle \mathbb {R} ^{2}}$${\textstyle x_{1}\leq 3}$${\textstyle x_{1}\geq 4}$

Figura que se muestra y que contiene la primera figura${\textstyle \mathbb {R} ^{2}}$${\textstyle x_{1}\leq 3}$${\textstyle x_{1}\leq 4}$

Figura en la que se muestra , y sus intersecciones${\textstyle \mathbb {R} ^{2}}$${\textstyle x_{1}\leq 3}$${\textstyle x_{2}\geq -3}$

Figura en la que se muestra , y sus intersecciones${\textstyle \mathbb {R} ^{2}}$${\textstyle x_{1}\leq 3}$${\textstyle x_{1}\leq x_{2}+3}$