Región (verificación de modelos)

En la verificación de modelos , un campo de la informática , una región es un politopo convexo de alguna dimensión , y más precisamente una zona , que satisface alguna propiedad de minimalidad. Las regiones son particiones . ${\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 modo que si dos vectores y pertenecen a la misma región, entonces satisfacen las mismas restricciones de . Además, cuando esos vectores se consideran como una tupla de relojes , ambos vectores tienen el mismo conjunto de futuros posibles. Intuitivamente, significa que cualquier lógica temporal proposicional temporizada -fórmula, o autómata temporizado o autómata de señales que use 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 regiones permite crear el autómata de región , que es un grafo dirigido en el que cada nodo es una región, y cada arista asegura que es un futuro posible 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 no temporizado . En particular, permite reducir el problema de vacío para al problema de vacío para un autómata finito o Büchi. Esta técnica es utilizada por ejemplo por el software UPPAAL . ^[1] ${\displaystyle r\to r'}$ ${\displaystyle r'}$ ${\displaystyle r}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle L}$ ${\displaystyle L}$ ${\displaystyle {\mathcal {A}}}$

Definición

Sea un conjunto de relojes . Para cada sea . Intuitivamente, este número representa un límite superior de los valores con los que se puede comparar el reloj. La definición de una región sobre los relojes de utiliza esos números . A continuación se dan tres definiciones equivalentes. ${\displaystyle C=\{x_{1},\dots ,x_{d}\}}$ ${\displaystyle x\in \mathbb {N} }$ ${\displaystyle c_{x}\in \mathbb {N} }$ ${\displaystyle x}$ ${\displaystyle C}$ ${\displaystyle c_{x}}$

Dada una asignación de reloj , denota la región a la que pertenece. El conjunto de regiones se denota por . ${\displaystyle \nu }$ ${\displaystyle [\nu ]}$ ${\displaystyle \nu }$ ${\displaystyle {\mathcal {R}}}$

Asignación de equivalencia de relojes

La primera definición permite probar fácilmente si dos asignaciones pertenecen a la misma región.

Una región puede definirse como una clase de equivalencia para alguna relación de equivalencia. Dos asignaciones de relojes y son equivalentes si satisfacen las siguientes restricciones: ^{[2] : 202} ${\displaystyle \nu _{1}}$ ${\displaystyle \nu _{2}}$

• ${\displaystyle \nu _{1}(x)\sim c}$si y solo si , para cada uno y un entero, y ~ es una de las siguientes relaciones = , < o ≤ . ${\displaystyle \nu _{2}(x)\sim c}$ ${\displaystyle x\in C}$ ${\displaystyle 0\leq c\leq c_{x}}$
• ${\displaystyle \{\nu _{1}(x)\}\sim \{\nu _{1}(y)\}}$si y solo si , para cada , , , siendo la parte fraccionaria del real , y ~ siendo una de las siguientes relaciones = , < o ≤ . ${\displaystyle \{\nu _{2}(x)\}\sim \{\nu _{2}(y)\}}$ ${\displaystyle x,y\in C}$ ${\displaystyle \nu _{1}(x)\leq c_{x}}$ ${\displaystyle \nu _{1}(y)\leq c_{y}}$ ${\displaystyle \{r\}}$ ${\displaystyle r}$

El primer tipo de restricciones garantiza que y satisface las mismas restricciones. De hecho, si y , entonces solo la segunda asignación satisface . Por otro lado, si y , ambas asignaciones satisfacen exactamente el mismo conjunto de restricciones, ya que las restricciones usan solo constantes integrales. ${\displaystyle \nu _{1}}$ ${\displaystyle \nu _{2}}$ ${\displaystyle \nu _{1}(x)=0.5}$ ${\displaystyle \nu _{2}(x)=1}$ ${\displaystyle x=1}$ ${\displaystyle \nu _{1}(x)=0.5}$ ${\displaystyle \nu _{2}(x)=0.6}$

El segundo tipo de restricciones garantiza que el futuro de dos asignaciones satisfaga las mismas restricciones. Por ejemplo, sea y . Entonces, la restricción se satisface eventualmente para el futuro de sin reinicio del reloj, pero no para el futuro de sin reinicio del reloj. ${\displaystyle \nu _{1}=\{x\mapsto 0.5,y\mapsto 0.6\}}$ ${\displaystyle \nu _{2}=\{x\mapsto 0.5,y\mapsto 0.4\}}$ ${\displaystyle y=1\land x<1}$ ${\displaystyle \nu _{1}}$ ${\displaystyle \nu _{2}}$

Definición explícita de una región

Si bien la definición anterior permite comprobar si dos asignaciones pertenecen a la misma región, no permite representar fácilmente una región como una estructura de datos. La tercera definición que se proporciona a continuación permite dar una codificación canónica de una región.

Una región puede definirse explícitamente como una zona, utilizando un conjunto de ecuaciones e inecuaciones que satisfacen las siguientes restricciones: ${\displaystyle S}$

• Para cada uno , contiene: ${\displaystyle x\in C}$ ${\displaystyle S}$
  • ${\displaystyle x=c}$para algún entero ${\displaystyle 0\leq c\leq c_{x}}$
  • ${\displaystyle x\in (c,c+1)}$para algún entero , ${\displaystyle 0\leq c<c_{x}}$
  • ${\displaystyle x>c_{x}}$,
• además, para cada par de relojes , donde contiene restricciones de la forma y , entonces contiene una (in)igualdad de la forma con siendo = , < o ≤ . ${\displaystyle x,y\in C}$ ${\displaystyle S}$ ${\displaystyle x\in (c,c+1)}$ ${\displaystyle y\in (c',c'+1)}$ ${\displaystyle S}$ ${\displaystyle \{x\}\sim \{y\}}$ ${\displaystyle \sim }$

Dado que, cuando y son fijos, la última restricción es equivalente a . ${\displaystyle c}$ ${\displaystyle c'}$ ${\displaystyle x\sim y+c-c'}$

Esta definición permite codificar una región como una estructura de datos. Basta, para cada reloj, indicar a qué intervalo pertenece y recordar el orden de la parte fraccionaria de los relojes que pertenecen a un intervalo abierto de longitud 1. De ello se deduce que el tamaño de esta estructura es proporcional al número de relojes. ${\displaystyle O\left(\sum \log(c_{k})+|C|\log(|C|)\right)}$ ${\displaystyle |C|}$

Bisimulación temporizada

Ahora, demos una tercera definición de regiones. Si bien esta definición es más abstracta, también es la razón por la que se utilizan regiones en la verificación de modelos. Intuitivamente, esta definición establece que dos asignaciones de reloj pertenecen a la misma región si las diferencias entre ellas son tales que ningún autómata cronometrado puede notarlas. Dada cualquier ejecución que comience con una asignación de reloj , para cualquier otra asignación en la misma región, hay una ejecución , que pasa por las mismas ubicaciones, lee las mismas letras, donde la única diferencia es que el tiempo esperado entre dos transiciones sucesivas puede ser diferente y, por lo tanto, las variaciones sucesivas del reloj son diferentes. ${\displaystyle r}$ ${\displaystyle \nu }$ ${\displaystyle \nu '}$ ${\displaystyle r'}$

Ahora se da la definición formal. Dado un conjunto de relojes , dos asignaciones dos asignaciones de relojes y pertenece a la misma región si para cada autómata temporizado en el que los guardias nunca comparan un reloj con un número mayor que , dada cualquier ubicación de , existe una bisimulación temporizada entre los estados extendidos y . Más precisamente, esta bisimulación conserva letras y ubicaciones pero no las asignaciones de relojes exactas. ^{[1] : 7} ${\displaystyle C}$ ${\displaystyle \nu _{1}}$ ${\displaystyle \nu _{2}}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle x}$ ${\displaystyle c_{x}}$ ${\displaystyle \ell }$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle (\ell ,\nu _{1})}$ ${\displaystyle (\ell ,\nu _{2})}$

Operación en regiones

Algunas operaciones ahora están definidas sobre regiones: reiniciar parte de su reloj y dejar pasar el tiempo.

Reinicio de relojes

Dada una región definida por un conjunto de (in)ecuaciones y un conjunto de relojes , ahora se define la región similar a en la que se reinician los relojes de . Esta región se denota por , y se define por las siguientes restricciones: ${\displaystyle \alpha }$ ${\displaystyle S}$ ${\displaystyle C'\subseteq C}$ ${\displaystyle \alpha }$ ${\displaystyle C'}$ ${\displaystyle \alpha [C'\mapsto 0]}$

• cada una de las restricciones de no contener el reloj , ${\displaystyle S}$ ${\displaystyle x}$
• las restricciones para . ${\displaystyle x=0}$ ${\displaystyle x\in C'}$

El conjunto de asignaciones definido por es exactamente el conjunto de asignaciones para . ${\displaystyle \alpha [C'\mapsto 0]}$ ${\displaystyle \nu [C'\mapsto 0]}$ ${\displaystyle \nu \in \alpha }$

Sucesor del tiempo

Dada una región , las regiones a las que se puede llegar sin reiniciar un reloj se denominan sucesores temporales de . A continuación se dan dos definiciones equivalentes. ${\displaystyle \alpha }$ ${\displaystyle \alpha }$

Definición

Una región de reloj es un sucesor temporal de otra región de reloj si para cada asignación , existe algún real positivo tal que . ${\displaystyle \alpha '}$ ${\displaystyle \alpha }$ ${\displaystyle \nu \in \alpha }$ ${\displaystyle t_{\nu ,\alpha '}>0}$ ${\displaystyle \nu +t_{\nu ,\alpha '}\in \alpha '}$

Obsérvese que esto no significa que . Por ejemplo, la región definida por el conjunto de restricciones tiene el sucesor temporal definido por el conjunto de restricciones . De hecho, para cada , basta con tomar . Sin embargo, no existe ningún real tal que o incluso tal que ; de hecho, define un triángulo mientras que define un segmento. ${\displaystyle \alpha +t_{\nu ,\alpha '}=\alpha '}$ ${\displaystyle \alpha }$ ${\displaystyle \{0<x<1,0<y<1,x<y\}}$ ${\displaystyle \alpha '}$ ${\displaystyle \{0<x<1,y=1\}}$ ${\displaystyle \nu \in \alpha }$ ${\displaystyle t_{\nu ,\alpha '}=1-\nu (y)}$ ${\displaystyle t}$ ${\displaystyle \alpha +t=\alpha '}$ ${\displaystyle \alpha +t\subseteq \alpha '}$ ${\displaystyle \alpha }$ ${\displaystyle \alpha '}$

Definición computable

La segunda definición dada ahora permite calcular explícitamente el conjunto de sucesores temporales de una región, dado por su conjunto de restricciones.

Dada una región definida como un conjunto de restricciones , definamos su conjunto de sucesores temporales. Para ello, se requieren las siguientes variables. Sea el conjunto de restricciones de de la forma . Sea el conjunto de relojes tales que contiene la restricción . Sea el conjunto de relojes tales que no hay restricciones de la forma en . ${\displaystyle \alpha }$ ${\displaystyle S}$ ${\displaystyle T\subseteq S}$ ${\displaystyle S}$ ${\displaystyle x_{i}=c_{i}}$ ${\displaystyle Y\subseteq C}$ ${\displaystyle y}$ ${\displaystyle S}$ ${\displaystyle y>c_{y}}$ ${\displaystyle Z\subseteq C\setminus Y}$ ${\displaystyle \{z\}}$ ${\displaystyle \{x\}<\{z\}}$ ${\displaystyle S}$

Si está vacío, es su propio sucesor temporal. Si , entonces es el único sucesor temporal de . De lo contrario, existe un sucesor temporal menor de distinto de . El sucesor temporal menor, si no está vacío, contiene: ${\displaystyle T}$ ${\displaystyle \alpha }$ ${\displaystyle Y=C}$ ${\displaystyle \alpha }$ ${\displaystyle \alpha }$ ${\displaystyle \alpha }$ ${\displaystyle \alpha }$ ${\displaystyle T}$

• Las limitaciones de ${\displaystyle S\setminus T}$
• ${\displaystyle x_{i}>c_{i}}$,
• ${\displaystyle \{x_{i}\}=\{x_{j}\}}$, y
• para cada uno que no pertenece a , la restricción . ${\displaystyle y}$ ${\displaystyle y>c_{y}}$ ${\displaystyle S}$ ${\displaystyle x_{i}<y}$

Si está vacío, el sucesor temporal mínimo se define mediante las siguientes restricciones: ${\displaystyle T}$

• las limitaciones de no utilizar los relojes de , ${\displaystyle S}$ ${\displaystyle Z}$
• la restricción , para cada restricción en , con . ${\displaystyle z=c+1}$ ${\displaystyle c<z<c+1}$ ${\displaystyle S}$ ${\displaystyle z\in Z}$

Propiedades

Hay en la mayoría de las regiones, donde es el número de relojes. ^{[2] : 203} ${\displaystyle |C|!2^{|C|}\prod _{x\in C}(2c_{x}+2)}$ ${\displaystyle |C|}$

Autómata de región

Dado un autómata cronometrado , su autómata de región es un autómata finito o un autómata de Büchi que acepta . Este autómata es similar a , donde los relojes se reemplazan por región. Intuitivamente, el autómata de región se construye como un producto de y del gráfico de región. Este gráfico de región se define primero. ${\displaystyle {\mathcal {A}}}$ ${\displaystyle L}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle {\mathcal {A}}}$

Gráfica de regiones

El gráfico de región es un gráfico dirigido con raíz que modela el conjunto de posibles valores de reloj durante la ejecución de un temporizador automático temporizado. Se define de la siguiente manera:

• sus nodos son regiones,
• Su raíz es la región inicial , definida por el conjunto de restricciones , ${\displaystyle \alpha _{0}}$ ${\displaystyle \{x=0\mid x\in C\}}$
• el conjunto de aristas son , para un sucesor temporal de . ${\displaystyle (\alpha ,\alpha '[C'\mapsto 0])}$ ${\displaystyle \alpha '}$ ${\displaystyle \alpha }$

Autómata de región

Sea un autómata temporizado . Para cada reloj , sea el mayor número tal que exista un guarda de la forma en . El autómata de región de , denotado por es un autómata finito o de Büchi que es esencialmente un producto de y del gráfico de región definido anteriormente. Es decir, cada estado del autómata de región es un par que contiene una ubicación de y una región. Dado que la asignación de dos relojes que pertenecen a la misma región satisface el mismo guarda, cada región contiene suficiente información para decidir qué transiciones se pueden tomar. ${\displaystyle {\mathcal {A}}=\langle \Sigma ,L,L_{0},C,F,E\rangle }$ ${\displaystyle x\in C}$ ${\displaystyle c_{x}}$ ${\displaystyle c}$ ${\displaystyle x\sim c}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle R({\mathcal {A}})}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle {\mathcal {A}}}$

Formalmente, el autómata de región se define de la siguiente manera:

• Su alfabeto es , ${\displaystyle \Sigma }$
• Su conjunto de estados es , ${\displaystyle L\times {\mathcal {R}}}$
• Su conjunto de estados está con la región inicial, ${\displaystyle L_{0}\times \{\alpha _{0}\}}$ ${\displaystyle \alpha _{0}}$
• Su conjunto de estados de aceptación es , ${\displaystyle F\times {\mathcal {R}}}$
• Su relación de transición contiene , para , tal que y es un sucesor temporal de . ${\displaystyle \delta }$ ${\displaystyle ((\ell ,\alpha ),a,(\ell ',\alpha '[C'\mapsto 0]))}$ ${\displaystyle (\ell ,a,g,C',\ell ')\in E}$ ${\displaystyle \gamma \models \alpha '}$ ${\displaystyle \alpha '}$ ${\displaystyle \alpha }$

Dada cualquier ejecución de , la secuencia se denota , es una ejecución de y acepta si y solo si acepta ^{[2] : 207} . De ello se deduce que . En particular, acepta una palabra cronometrada si y solo si acepta una palabra. Además, una ejecución de aceptación de se puede calcular a partir de una ejecución de aceptación de . ${\displaystyle r=(\ell _{0},\nu _{0}){\xrightarrow[{t_{1}}]{\sigma _{1}}}(\ell _{1},\nu _{1})\dots }$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle (\ell _{0},[\nu _{0}]){\xrightarrow {\sigma _{1}}}(\ell _{1},[\nu _{1}])\dots }$ ${\displaystyle [r]}$ ${\displaystyle R({\mathcal {A}})}$ ${\displaystyle r}$ ${\displaystyle L(R({\mathcal {A}}))=\operatorname {Untime} (L({\mathcal {A}}))}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle R({\mathcal {A}})}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle R({\mathcal {A}})}$

Referencias

1. Bengtsson, Johan; Yi, Wang L (2004). "Autómatas temporizados: semántica, algoritmos y herramientas". Lecciones sobre concurrencia y redes de Petri . Apuntes de clase en informática. Vol. 3098. págs. 87–124. doi :10.1007/978-3-540-27755-2_3. ISBN 978-3-540-22261-3.
2. Alur, Rajeev; Dill, David L (25 de abril de 1994). "Una teoría de autómatas temporizados" (PDF) . Theoretical Computer Science . 126 (2): 183–235. doi : 10.1016/0304-3975(94)90010-8 .