Matriz de diferencia límite

En la verificación de modelos , un campo de la informática , una matriz de límites diferenciales (DBM) es una estructura de datos que se utiliza para representar algunos politopos convexos llamados zonas . Esta estructura se puede utilizar 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 verificador de modelos Uppaal , donde también se distribuye como una biblioteca independiente. ^[1]

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

Zona

Una matriz de límites diferenciales se utiliza para representar algún tipo de politopos convexos. Esos politopos se denominan zona . Ahora están definidos. Formalmente, una zona se define mediante ecuaciones de la forma , , y , con y algunas variables y una constante. ${\displaystyle x\leq c}$ ${\displaystyle x\geq c}$ ${\displaystyle x_{1}\leq x_{2}+c}$ ${\displaystyle x_{1}\geq x_{2}+c}$ ${\displaystyle x_{1}}$ ${\displaystyle x_{2}}$ ${\displaystyle c}$

Las zonas se denominaban originalmente región ^[2], pero hoy en día este nombre suele denotar 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 utilizan una única variable y un límite superior, restricciones que utilizan una única 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 en puede requerir un número arbitrario de restricciones. Incluso cuando , puede haber un número arbitrario de restricciones no redundantes , para algunas constantes. Esta es la razón por la que los DBM no se pueden extender desde zonas a politopos convexos. ${\displaystyle n}$ ${\displaystyle n(n+1)}$ ${\displaystyle n}$ ${\displaystyle n}$ ${\displaystyle n^{2}}$ ${\displaystyle (x,y)}$ ${\displaystyle x-y}$ ${\displaystyle \mathbb {R} ^{n}}$ ${\displaystyle n=2}$ ${\displaystyle (x<iy+c_{i})_{i\in \mathbb {N} }}$ ${\displaystyle c_{i}}$

Ejemplo

Como se indicó en la introducción, consideramos una zona definida por un conjunto de enunciados de la forma , , y , con y algunas variables, y una constante. Sin embargo, algunas de esas restricciones son contradictorias o redundantes. A continuación, presentamos ejemplos de este tipo. ${\displaystyle x_{1}\leq c}$ ${\displaystyle x_{1}\geq c}$ ${\displaystyle x_{1}\leq x_{2}+c}$ ${\displaystyle x_{1}\geq x_{2}+c}$ ${\displaystyle x_{1}}$ ${\displaystyle x_{2}}$ ${\displaystyle c}$

• Las restricciones y son contradictorias. Por lo tanto, cuando se encuentran dos restricciones de este tipo, la zona definida está vacía. ${\displaystyle x_{1}\leq 3}$ ${\displaystyle x_{1}\geq 4}$

  

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

• Las restricciones y son redundantes. La segunda restricción está implícita en la primera. Por lo tanto, cuando se encuentran dos restricciones de este tipo en la definición de la zona, se puede eliminar la segunda restricción. ${\displaystyle x_{1}\leq 3}$ ${\displaystyle x_{1}\leq 4}$

  

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

También damos un ejemplo que muestra cómo generar nuevas restricciones a partir de restricciones existentes. Para cada par de relojes y , el DBM tiene una restricción de la forma , donde es < o ≤. Si no se puede encontrar dicha restricción, la restricción se puede agregar a la definición de zona sin pérdida de generalidad. Pero en algunos casos, se puede encontrar una restricción más precisa. A continuación se dará un ejemplo de este tipo. ${\displaystyle x_{1}}$ ${\displaystyle x_{2}}$ ${\displaystyle x_{1}\prec x_{2}+c}$ ${\displaystyle \prec }$ ${\displaystyle x_{1}\prec x_{2}+\infty }$

• Las restricciones , implican que . Por lo tanto, suponiendo que ninguna otra restricción como o pertenece a la definición, la restricción se agrega a la definición de la zona. ${\displaystyle x_{1}\leq 3}$ ${\displaystyle x_{2}\geq -3}$ ${\displaystyle x_{1}\leq x_{2}+6}$ ${\displaystyle x_{1}\leq x_{2}+5}$ ${\displaystyle x_{1}<x_{2}+6}$ ${\displaystyle x_{1}\leq x_{2}+6}$

  

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

• Las restricciones , implican que . Por lo tanto, suponiendo que ninguna otra restricción como o pertenece a la definición, la restricción se agrega a la definición de la zona. ${\displaystyle x_{2}\leq 3}$ ${\displaystyle x_{1}\leq x_{2}+3}$ ${\displaystyle x_{1}\leq 6}$ ${\displaystyle x_{1}\leq 5}$ ${\displaystyle x_{1}<6}$ ${\displaystyle x_{1}\leq 6}$

  

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

• Las restricciones , implican que . Por lo tanto, suponiendo que ninguna otra restricción como o pertenece a la definición, la restricción se agrega a la definición de la zona. ${\displaystyle x_{1}\leq x_{2}+3}$ ${\displaystyle x_{2}\leq x_{3}+3}$ ${\displaystyle x_{1}\leq x_{3}+6}$ ${\displaystyle x_{1}\leq x_{3}+5}$ ${\displaystyle x_{1}<x_{3}+6}$ ${\displaystyle x_{1}\leq x_{3}+6}$

En realidad, los dos primeros casos anteriores son casos particulares de los terceros casos. De hecho, y pueden reescribirse como y respectivamente. Por lo tanto, la restricción agregada en el primer ejemplo es similar a la restricción agregada en el tercer ejemplo. ${\displaystyle x_{1}\leq 3}$ ${\displaystyle x_{2}\geq -3}$ ${\displaystyle x_{1}\leq 0+3}$ ${\displaystyle 0\leq x_{2}+3}$ ${\displaystyle x_{1}\leq x_{2}+6}$

Definición

Ahora fijamos un monoide que es un subconjunto de la recta real. Este monoide es tradicionalmente el conjunto de números enteros , racionales , reales o su subconjunto de números no negativos. ${\displaystyle (M,0,+)}$

Restricciones

Para definir la estructura de datos de la matriz de límites diferenciales , primero se requiere proporcionar una estructura de datos para codificar las restricciones atómicas. Además, introducimos un álgebra para las restricciones atómicas. Esta álgebra es similar al semianillo tropical , con dos modificaciones:

• Se puede utilizar un monoide ordenado arbitrario en lugar de . ${\displaystyle \mathbb {R} }$
• Para distinguir entre " " y " ", el conjunto de elementos del álgebra debe contener información que indique si el orden es estricto o no. ${\displaystyle <m}$ ${\displaystyle \leq m}$

Definición de restricciones

El conjunto de restricciones satisfacibles se define como el conjunto de pares de la forma:

• ${\displaystyle (\leq ,m)}$, con , que representa una restricción de la forma , ${\displaystyle m\in M}$ ${\displaystyle \leq m}$
• ${\displaystyle (<,m)}$, con , donde no es un elemento mínimo de , lo que representa una restricción de la forma , ${\displaystyle m\in M}$ ${\displaystyle m}$ ${\displaystyle M}$ ${\displaystyle <m}$
• ${\displaystyle (<,\infty )}$, lo que representa la ausencia de restricción.

El conjunto de restricciones contiene todas las restricciones satisfacibles y también contiene la siguiente restricción insatisfacible:

• ${\displaystyle (<,-\infty )}$.

El subconjunto no se puede definir utilizando este tipo de restricciones. En términos más generales, algunos politopos convexos no se pueden definir cuando el monoide ordenado no tiene la propiedad de límite superior mínimo , incluso si cada una de las restricciones en su definición utiliza como máximo dos variables. ${\displaystyle \{q\in \mathbb {Q} \mid q\leq {\sqrt {2}}\}}$

Operación sobre restricciones

Para generar una única restricción a partir de un par de restricciones aplicadas al mismo par de variables, formalizamos la noción de intersección de restricciones y de orden sobre restricciones. De manera similar, para definir una nueva restricción a partir de restricciones existentes, también debe definirse una noción de suma de restricciones.

Orden sobre restricciones

Definimos ahora una relación de orden sobre restricciones. Este orden simboliza la relación de inclusión.

En primer lugar, el conjunto se considera un conjunto ordenado, donde < es inferior a ≤. Intuitivamente, se elige este orden porque el conjunto definido por está estrictamente incluido en el conjunto definido por . Entonces, afirmamos que la restricción es menor que si o ( y es menor que ). Es decir, el orden de las restricciones es el orden lexicográfico aplicado de derecha a izquierda. Nótese que este orden es un orden total . Si tiene la propiedad de límite superior mínimo (o propiedad de límite inferior máximo ), entonces el conjunto de restricciones también la tiene. ${\displaystyle \{<,\leq \}}$ ${\displaystyle x<c}$ ${\displaystyle x\leq c}$ ${\displaystyle (\prec _{1},m_{1})}$ ${\displaystyle (\prec _{2},m_{2})}$ ${\displaystyle m_{1}<m_{2}}$ ${\displaystyle m_{1}=m_{2}}$ ${\displaystyle \prec _{1}}$ ${\displaystyle \prec _{2}}$ ${\displaystyle M}$

Intersección de restricciones

La intersección de dos restricciones, denotada como , se define entonces simplemente como el mínimo de esas dos restricciones. Si tiene la propiedad de límite inferior máximo, entonces también se define la intersección de un número infinito de restricciones. ${\displaystyle (\prec _{1},m_{1})\sqcap (\prec _{2},m_{2})}$ ${\displaystyle M}$

Suma de restricciones

Dadas dos variables y a las que se aplican las restricciones y , ahora explicamos cómo generar la restricción satisfecha por . Esta restricción se denomina suma de las dos restricciones mencionadas anteriormente, se denota como y se define como . ${\displaystyle x_{1}}$ ${\displaystyle x_{2}}$ ${\displaystyle (\prec _{1},m_{1})}$ ${\displaystyle (\prec _{2},m_{2})}$ ${\displaystyle x_{1}+x_{2}}$ ${\displaystyle (\prec _{1},m_{1})+(\prec _{2},m_{2})}$ ${\displaystyle (\min(\prec _{1},\prec _{2}),m_{1}+m_{2})}$

Las restricciones como álgebra

Aquí hay una lista de propiedades algebraicas satisfechas por el conjunto de restricciones.

• Ambas operaciones son asociativas y conmutativas ,
• La suma es distributiva sobre la intersección, es decir, para tres restricciones cualesquiera, es igual a , ${\displaystyle ((\prec _{1},m_{1})\sqcap (\prec _{2},m_{2}))+(\prec _{3},m_{3})}$ ${\displaystyle ((\prec _{1},m_{1})+(\prec _{3},m_{3}))\sqcap ((\prec _{2},m_{2})+(\prec _{3},m_{3}))}$
• La operación de intersección es idempotente,
• La restricción es una identidad para la operación de intersección, ${\displaystyle (<,\infty )}$
• La restricción es una identidad para la operación de suma, ${\displaystyle (\leq ,0)}$

Además, las siguientes propiedades algebraicas se cumplen en condiciones de restricción satisfacibles:

• La restricción es cero para la operación de suma, ${\displaystyle (<,\infty )}$
• De ello se deduce que el conjunto de restricciones satisfacibles es un semianillo idempotente , con como cero y como unidad. ${\displaystyle (<,\infty )}$ ${\displaystyle (\leq ,0)}$
• Si 0 es el elemento mínimo de , entonces es un cero para las restricciones de intersección sobre restricciones satisfacibles. ${\displaystyle M}$ ${\displaystyle (\leq ,0)}$

Sobre restricciones no satisfacibles ambas operaciones tienen el mismo cero, que es . Por lo tanto, el conjunto de restricciones ni siquiera forma un semianillo, porque la identidad de la intersección es distinta del cero de la suma. ${\displaystyle (<,-\infty )}$

DBM

Dado un conjunto de variables, , un DBM es una matriz con columnas y filas indexadas por y las entradas son restricciones. Intuitivamente, para una columna y una fila , el valor en la posición representa . Por lo tanto, la zona definida por una matriz , denotada por , es . ${\displaystyle n}$ ${\displaystyle x_{1},\dots ,x_{n}}$ ${\displaystyle 0,x_{1},\dots ,x_{n}}$ ${\displaystyle C}$ ${\displaystyle R}$ ${\displaystyle m}$ ${\displaystyle (C,R)}$ ${\displaystyle C\prec R+m}$ ${\displaystyle D((\prec _{C,R},m_{C,R}))_{C,R\in \{0,x_{1},\dots ,x_{n}}\}}$ ${\displaystyle {\mathcal {R}}(D)}$ ${\displaystyle \{(x_{1},\dots ,x_{n})\in \mathbb {R} \mid \bigwedge _{C,R\in \{0,x_{1},\dots ,x_{n}\}}C\prec _{C,R}R+m_{C,R}\}}$

Nótese que es equivalente a , por lo tanto, la entrada sigue siendo esencialmente un límite superior. Sin embargo, nótese que, dado que consideramos un monoide , para algunos valores de y el real en realidad no pertenece al monoide. ${\displaystyle C\prec R+m}$ ${\displaystyle C-R\prec m}$ ${\displaystyle (\prec ,m)}$ ${\displaystyle M}$ ${\displaystyle C}$ ${\displaystyle R}$ ${\displaystyle C-R}$

Antes de introducir la definición de un DBM canónico, necesitamos definir y discutir una relación de orden en esas matrices.

Orden en esas matrices

Se considera que una matriz es más pequeña que una matriz si cada una de sus entradas es más pequeña. Nótese que este orden no es total. Dados dos DBM y , si es menor o igual que , entonces . ${\displaystyle D}$ ${\displaystyle D'}$ ${\displaystyle D}$ ${\displaystyle D'}$ ${\displaystyle D}$ ${\displaystyle D'}$ ${\displaystyle {\mathcal {R}}(D)\subseteq {\mathcal {R}}(D')}$

El límite inferior máximo de dos matrices y , denotado por , tiene como entrada el valor . Nótese que como es la operación de «suma» del semianillo de restricciones, la operación es la «suma» de dos DBM donde el conjunto de DBM se considera como un módulo . ${\displaystyle D}$ ${\displaystyle D'}$ ${\displaystyle D\sqcap D'}$ ${\displaystyle (a,b)}$ ${\displaystyle (\prec _{a,b},m_{a,b})\sqcap (\prec '_{a,b},m'_{a,b})}$ ${\displaystyle \sqcap }$ ${\displaystyle \sqcap }$

De manera similar al caso de las restricciones, considerado en la sección "Operación sobre restricciones" anterior, el límite inferior máximo de un número infinito de matrices se define correctamente tan pronto como satisface la propiedad del límite inferior máximo. ${\displaystyle M}$

La intersección de matrices/zonas está definida. La operación de unión no está definida y, de hecho, una unión de zonas no es una zona en general.

Para un conjunto arbitrario de matrices que definen la misma zona , también define . De ello se deduce que, siempre que tenga la propiedad de límite inferior máximo, cada zona que esté definida por al menos una matriz tiene una matriz mínima única que la define. Esta matriz se denomina matriz mínima canónica de . ${\displaystyle {\mathcal {D}}}$ ${\displaystyle Z}$ ${\displaystyle \sqcap _{D\in {\mathcal {D}}}D}$ ${\displaystyle Z}$ ${\displaystyle M}$ ${\displaystyle Z}$

Primera definición de DBM canónico

Reafirmamos la definición de una matriz de límite diferencial canónico . Es una matriz de límite diferencial tal que ninguna matriz más pequeña define el mismo conjunto. A continuación se explica cómo comprobar si una matriz es una matriz de límite diferencial y, en caso contrario, cómo calcular una matriz de límite diferencial a partir de una matriz arbitraria de modo que ambas matrices representen el mismo conjunto. Pero primero, daremos algunos ejemplos.

Ejemplos de matrices

Consideremos primero el caso en el que hay un solo reloj . ${\displaystyle x_{1}}$

La linea real

Primero damos el DBM canónico para . Luego introducimos otro DBM que codifica el conjunto . Esto permite encontrar restricciones que debe cumplir cualquier DBM. ${\displaystyle \mathbb {R} }$ ${\displaystyle \mathbb {R} }$

El DBM canónico del conjunto de los reales es . Representa las restricciones , , y . Todas esas restricciones se satisfacen independientemente del valor asignado a . En el resto de la discusión, no describiremos explícitamente las restricciones debidas a entradas de la forma , ya que esas restricciones se satisfacen sistemáticamente. ${\displaystyle \left({\begin{array}{ll}(\leq ,0)&(<,\infty )\\(<,\infty )&(\leq ,0)\end{array}}\right)}$ ${\displaystyle 0\leq 0+0}$ ${\displaystyle x_{1}\leq 0+\infty }$ ${\displaystyle 0\leq x_{1}+\infty }$ ${\displaystyle 0\leq 0+0}$ ${\displaystyle x_{1}}$ ${\displaystyle (<,\infty )}$

El DBM también codifica el conjunto de los valores reales. Contiene las restricciones y que se satisfacen independientemente del valor de . Esto demuestra que en un DBM canónico , una entrada diagonal nunca es mayor que , porque la matriz obtenida de al reemplazar la entrada diagonal por define el mismo conjunto y es menor que . ${\displaystyle \left({\begin{array}{ll}(<,\infty )&(<,\infty )\\(<,\infty )&(<,\infty )\end{array}}\right)}$ ${\displaystyle 0<0+\infty }$ ${\displaystyle x_{1}<x_{1}+\infty }$ ${\displaystyle x_{1}}$ ${\displaystyle D}$ ${\displaystyle (\leq ,0)}$ ${\displaystyle D}$ ${\displaystyle (\leq ,0)}$ ${\displaystyle D}$

El conjunto vacío

Ahora consideramos muchas matrices que codifican el conjunto vacío. Primero damos el DBM canónico para el conjunto vacío. Luego explicamos por qué cada uno de los DBM codifica el conjunto vacío. Esto permite encontrar restricciones que deben ser satisfechas por cualquier DBM.

El DBM canónico del conjunto vacío, sobre una variable, es . De hecho, representa el conjunto que satisface la restricción , , y . Esas restricciones son insatisfacibles. ${\displaystyle \left({\begin{array}{ll}(<,-\infty )&(<,-\infty )\\(<,-\infty )&(<,-\infty )\end{array}}\right)}$ ${\displaystyle 0<0-\infty }$ ${\displaystyle 0<x_{1}-\infty }$ ${\displaystyle x_{1}<0-\infty }$ ${\displaystyle x_{1}<x_{1}-\infty }$

El DBM también codifica el conjunto vacío. De hecho, contiene la restricción que es insatisfacible. En términos más generales, esto demuestra que ninguna entrada puede ser a menos que todas las entradas sean . ${\displaystyle \left({\begin{array}{ll}(<,\infty )&(<,-\infty )\\(<,\infty )&(<,\infty )\end{array}}\right)}$ ${\displaystyle x_{1}<0-\infty }$ ${\displaystyle (<,-\infty )}$ ${\displaystyle (<,-\infty )}$

El DBM también codifica el conjunto vacío. De hecho, contiene la restricción que es insatisfactoria. En términos más generales, esto demuestra que la entrada en la línea diagonal no puede ser menor que a menos que sea . ${\displaystyle \left({\begin{array}{ll}(<,\infty )&(<,\infty )\\(<,\infty )&(<,-1)\end{array}}\right)}$ ${\displaystyle x_{1}<x_{1}-1}$ ${\displaystyle (\leq ,0)}$ ${\displaystyle (<,-\infty )}$

El DBM también codifica el conjunto vacío. De hecho, contiene las restricciones y que son contradictorias. En términos más generales, esto demuestra que, para cada , si , entonces y son ambos iguales a ≤. ${\displaystyle \left({\begin{array}{ll}(<,\infty )&(<,1)\\(\leq ,-1)&(<,\infty )\end{array}}\right)}$ ${\displaystyle 0<x_{1}+1}$ ${\displaystyle x_{1}\leq -1}$ ${\displaystyle C,R\in \{0,x_{1},\dots ,x_{n}\}}$ ${\displaystyle m_{C,R}=-m_{R,C}}$ ${\displaystyle \prec _{R,C}}$ ${\displaystyle \prec _{C,R}}$

El DBM también codifica el conjunto vacío. De hecho, contiene las restricciones y que son contradictorias. En términos más generales, esto demuestra que para cada , , a menos que sea . ${\displaystyle \left({\begin{array}{ll}(<,\infty )&(\leq ,1)\\(\leq ,-2)&(<,\infty )\end{array}}\right)}$ ${\displaystyle 0\leq x_{1}+1}$ ${\displaystyle x_{1}\leq -2}$ ${\displaystyle C,R\in \{0,x_{1},\dots ,x_{n}\}}$ ${\displaystyle -m_{C,R}\leq m_{R,C}}$ ${\displaystyle m_{C,R}}$ ${\displaystyle -\infty }$

Restricciones estrictas

Los ejemplos que se dan en esta sección son similares a los ejemplos que se dan en la sección de Ejemplos anterior. Esta vez, se dan como DBM.

El DBM representa el conjunto que satisface las restricciones y . Como se mencionó en la sección de Ejemplos, ambas restricciones implican que . Significa que el DBM codifica la misma zona. En realidad, es el DBM de esta zona. Esto muestra que en cualquier DBM , para cada , la restricción es menor que la restricción . ${\displaystyle \left({\begin{array}{lll}(\leq ,0)&(<,\infty )&(<,\infty )\\(<,\infty )&(\leq ,0)&(\leq ,3)\\(\leq ,3)&(<,\infty )&(\leq ,0)\end{array}}\right)}$ ${\displaystyle x_{2}\leq 3}$ ${\displaystyle x_{1}\leq x_{2}+3}$ ${\displaystyle x_{1}\leq 6}$ ${\displaystyle \left({\begin{array}{lll}(\leq ,0)&(\leq ,6)&(<,\infty )\\(<,\infty )&(\leq ,0)&(\leq ,3)\\(\leq ,3)&(<,\infty )&(\leq ,0)\end{array}}\right)}$ ${\displaystyle ((\prec _{C,R},m_{C,R}))_{c,r\in \{0,x_{1},\dots ,x_{n}\}}}$ ${\displaystyle 1\leq i,j\leq n}$ ${\displaystyle (\prec _{x_{i},0},m_{x_{i},0})}$ ${\displaystyle (\prec _{x_{j},0},m_{x_{j},0})+(\prec _{x_{i},x_{j}},m_{x_{i},x_{j}})}$

Como se explica en la sección Ejemplo, la constante 0 puede considerarse como cualquier variable, lo que conduce a la regla más general: en cualquier DBM , para cada , la restricción es menor que la restricción . ${\displaystyle ((\prec _{C,R},m_{C,R}))_{c,r\in \{0,x_{1},\dots ,x_{n}\}}}$ ${\displaystyle a,b,c\in \{0,x_{1},\dots ,x_{n}\}}$ ${\displaystyle (\prec _{a,b},m_{a,b})}$ ${\displaystyle (\prec _{c,b},m_{c,b})+(\prec _{a,c},m_{a,c})}$

Tres definiciones de DBM canónico

Como se explica en la introducción de la sección Matriz de diferencias límite , un DBM canónico es un DBM cuyas filas y columnas están indexadas por , cuyas entradas son restricciones. Además, sigue una de las siguientes propiedades equivalentes. ${\displaystyle (0,x_{1},\dots ,x_{n})}$

• no hay DBM más pequeños que definan la misma zona,
• Para cada , la restricción es menor que la restricción ${\displaystyle a,b,c\in \{0,x_{1},\dots ,x_{n}\}}$ ${\displaystyle (\prec _{a,b},m_{a,b})}$ ${\displaystyle (\prec _{c,b},m_{c,b})+(\prec _{a,c},m_{a,c})}$
• Dado el gráfico dirigido con aristas y flechas etiquetadas con , el camino más corto desde cualquier arista a cualquier arista es la flecha . Este gráfico se denomina gráfico potencial del DBM. ${\displaystyle G}$ ${\displaystyle \{0,x_{1},\dots ,x_{n}\}}$ ${\displaystyle (a,b)}$ ${\displaystyle (\prec _{a,b},m_{a,b})}$ ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle (a,b)}$

La última definición se puede utilizar directamente para calcular el DBM canónico asociado a un DBM. Basta con aplicar el algoritmo Floyd-Warshall al grafo y asociar a cada entrada el camino más corto desde a en el grafo. Si este algoritmo detecta un ciclo de longitud negativa, significa que las restricciones no son satisfacibles y, por lo tanto, que la zona está vacía. ${\displaystyle (a,b)}$ ${\displaystyle a}$ ${\displaystyle b}$

Operaciones en zonas

Como se indica en la introducción, el principal interés de los DBM es que permiten implementar de forma fácil y eficiente operaciones en zonas.

Recordemos en primer lugar las operaciones que hemos considerado anteriormente:

• La prueba de inclusión de una zona en una zona se realiza comprobando si el DBM canónico de es menor o igual que el DBM de , ${\displaystyle Z_{1}}$ ${\displaystyle Z_{2}}$ ${\displaystyle Z_{1}}$ ${\displaystyle Z_{2}}$
• Un DBM para la intersección de un conjunto de zonas es el límite inferior máximo del DBM de esas zonas.
• La prueba de vacío de zona consiste en verificar si el DBM canónico de la zona consiste únicamente en , ${\displaystyle (<,-\infty )}$
• Probar si una zona es todo el espacio consiste en verificar si el DBM de la zona consta únicamente de . ${\displaystyle (<,\infty )}$

A continuación se describen las operaciones que no se han considerado anteriormente. Las primeras operaciones que se describen a continuación tienen un significado geométrico claro. Las últimas corresponden a operaciones que son más naturales para las valoraciones de relojes .

Suma de zonas

La suma de Minkowski de dos zonas, definidas por dos DBM y , está definida por el DBM cuya entrada es . Nótese que, dado que es la operación «producto» del semianillo de restricciones, la operación sobre DBM no es en realidad una operación del módulo de DBM. ${\displaystyle D}$ ${\displaystyle D'}$ ${\displaystyle D+D'}$ ${\displaystyle (a,b)}$ ${\displaystyle D_{a,b}+D'_{a,b}}$ ${\displaystyle +}$ ${\displaystyle +}$

En particular, se deduce que, para trasladar una zona por una dirección , basta con sumar el DBM de al DBM de . ${\displaystyle Z}$ ${\displaystyle v}$ ${\displaystyle \{v\}}$ ${\displaystyle Z}$

Proyección de un componente a un valor fijo

Sea una constante. ${\displaystyle d\in M}$

Dado un vector y un índice , la proyección del componente -ésimo de to es el vector . En el lenguaje del reloj, para , esto corresponde a reiniciar el -ésimo reloj. ${\displaystyle {\vec {x}}=(x_{1},\dots ,x_{n})}$ ${\displaystyle 1\leq i\leq n}$ ${\displaystyle i}$ ${\displaystyle {\vec {x}}}$ ${\displaystyle d}$ ${\displaystyle (x_{1},\dots ,x_{i-1},d,x_{i+1},\dots ,x_{n})}$ ${\displaystyle d=0}$ ${\displaystyle i}$

La proyección del componente -ésimo de una zona a consiste simplemente en el conjunto de vectores de con su componente -ésimo a . Esto se implementa en DBM configurando los componentes a y los componentes a ${\displaystyle i}$ ${\displaystyle Z}$ ${\displaystyle d}$ ${\displaystyle Z}$ ${\displaystyle i}$ ${\displaystyle d}$ ${\displaystyle (x_{i},a)}$ ${\displaystyle (\leq ,d)+D(0,a)}$ ${\displaystyle (a,x_{i})}$ ${\displaystyle (\leq ,-d)+D(0,a)}$

Futuro y pasado de una zona

Llamemos al futuro zona y al pasado zona . Dado un punto , el futuro de se define como , y el pasado de se define como . ${\displaystyle F=\{(t,\dots ,t)\mid t\in \mathbb {R} _{\geq 0}\}}$ ${\displaystyle P=\{(-t,\dots ,-t)\mid t\in \mathbb {R} _{\geq 0}\}}$ ${\displaystyle {\vec {x}}=(x_{1},\dots ,x_{n})\in \mathbb {R} ^{n}}$ ${\displaystyle {\vec {x}}}$ ${\displaystyle \{(x_{1}+t,\dots ,x_{n}+t)\mid t\in \mathbb {R} _{\geq 0}\}=F+\{{\vec {x}}\}}$ ${\displaystyle {\vec {x}}}$ ${\displaystyle P+\{{\vec {x}}\}}$

Los nombres futuro y pasado provienen de la noción de reloj . Si a un conjunto de relojes se les asignan los valores , , etc., entonces en su futuro, el conjunto de asignaciones que tendrán será el futuro de . ${\displaystyle n}$ ${\displaystyle x_{1}}$ ${\displaystyle x_{2}}$ ${\displaystyle {\vec {x}}}$

Dada una zona , el futuro de es la unión del futuro de cada uno de los puntos de la zona. La definición del pasado de una zona es similar. El futuro de una zona puede definirse como , y por lo tanto puede implementarse fácilmente como una suma de DBM. Sin embargo, hay un algoritmo aún más simple para aplicar a DBM. Basta con cambiar cada entrada a . De manera similar, el pasado de una zona puede calcularse estableciendo cada entrada a . ${\displaystyle Z}$ ${\displaystyle Z}$ ${\displaystyle F+Z}$ ${\displaystyle (x_{i},0)}$ ${\displaystyle (<,\infty )}$ ${\displaystyle (0,x_{i})}$ ${\displaystyle (<,\infty )}$

Véase también

• Región (verificación de modelo) : una zona, mínima bajo inclusión, que satisface algunas propiedades

Referencias

1. "Biblioteca UPPAAL DBM". GitHub . 16 de julio de 2021.
2. Dill, David L (1990). "Supuestos de temporización y verificación de sistemas concurrentes de estados finitos". Métodos de verificación automática para sistemas de estados finitos . Notas de clase en informática. Vol. 407. págs. 197–212. doi : 10.1007/3-540-52148-8_17 . ISBN. 978-3-540-52148-8.

• Matrices diferenciales ligadas Clase n.° 20 de Comprobación avanzada de modelos Joost-Pieter Katoen
• Péron, Mathias; Halbwachs, Nicolas (2008). "Un dominio abstracto que extiende matrices de límites diferenciales con restricciones de desigualdad" (PDF) . Verificación, comprobación de modelos e interpretación abstracta . Apuntes de clase en informática. Vol. 4349. págs. 268–282. doi : 10.1007/978-3-540-69738-1_20 . ISBN 978-3-540-69735-0.