Región (comprobación de modelo)

En la verificación de modelos , un campo de la informática , una región es un politopo convexo en alguna dimensión , y más precisamente una zona , que satisface alguna propiedad de minimidad. La partición de las regiones . ${\ Displaystyle \ mathbb {R} ^ {d}}$ ${\ Displaystyle d}$ ${\ Displaystyle \ mathbb {R} ^ {d}}$

El conjunto de zonas depende de un conjunto de restricciones de la forma,, y , con y algunas variables, y una constante. Las regiones se definen de manera que si dos vectores y pertenecen a la misma región, satisfacen las mismas restricciones de . Además, cuando esos vectores se consideran una tupla de relojes , ambos vectores tienen el mismo conjunto de posibles futuros. Intuitivamente, significa que cualquier fórmula lógica temporal proposicional cronometrada , o autómata cronometrado o autómata de señal que utilice solo las restricciones de no puede distinguir ambos vectores. ${\ Displaystyle K}$ ${\ 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}$ ${\ Displaystyle {\ vec {x}}}$ ${\ Displaystyle {\ vec {x}} '}$ ${\ Displaystyle K}$ ${\ Displaystyle K}$

El conjunto de región permite crear el autómata de región , que es un gráfico dirigido en el que cada nodo es una región, y cada borde asegura que es un posible futuro de . Tomando un producto de este autómata de región y de un autómata temporizado que acepta un lenguaje, se crea un autómata finito o un autómata Büchi que acepta sin tiempo . En particular, permite reducir el problema de la vacuidad al problema de la vacuidad para un autómata finito o Büchi. Esta técnica la utiliza, por ejemplo, el software UPPAAL . ^[1] ${\ Displaystyle r \ to r '}$ ${\ Displaystyle r '}$ ${\ Displaystyle r}$ ${\ Displaystyle {\ mathcal {A}}}$ ${\ Displaystyle L}$ ${\ Displaystyle L}$ ${\ Displaystyle {\ mathcal {A}}}$