Región (verificación de modelos)

La primera definición permite comprobar 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. Asignaciones de dos relojes${\displaystyle \nu _{1}}$y${\displaystyle \nu _{2}}$son equivalentes si satisfacen las siguientes restricciones: ^{[ 2 ] : 202}

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

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

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

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 presenta a continuación permite proporcionar una codificación canónica de una región.

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

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

Desde cuándo${\displaystyle c}$y${\displaystyle c'}$son fijos, la última restricción es equivalente a${\displaystyle x\sim y+c-c'}$.

Esta definición permite codificar una región como una estructura de datos. Basta, para cada reloj, con 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${\displaystyle O\left(\sum \log(c_{k})+|C|\log(|C|)\right)}$con${\displaystyle |C|}$el número de relojes.

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 temporizado puede detectarlas. Dado cualquier ejecución${\displaystyle r}$comenzando con una asignación de reloj${\displaystyle \nu }$, para cualquier otra tarea${\displaystyle \nu '}$En la misma región, hay una carrera${\displaystyle r'}$, pasando por los mismos lugares, leyendo 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.

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

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

• cada restricción de${\displaystyle S}$que no contiene el reloj${\displaystyle x}$,
• las restricciones${\displaystyle x=0}$para${\displaystyle x\in C'}$.

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

Dada una región${\displaystyle \alpha }$, las regiones que se pueden alcanzar sin reiniciar un reloj se denominan sucesores temporales de${\displaystyle \alpha }$Ahora se dan dos definiciones equivalentes.

El grafo de región es un grafo dirigido con raíz que modela el conjunto de posibles valores de reloj durante la ejecución de un autómata temporizado. Se define de la siguiente manera:

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

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

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 es${\displaystyle L_{0}\times \{\alpha _{0}\}}$con${\displaystyle \alpha _{0}}$la región inicial,
• su conjunto de estados aceptantes es${\displaystyle F\times {\mathcal {R}}}$,
• su relación de transición${\displaystyle \delta }$contiene ${\displaystyle ((\ell ,\alpha ),a,(\ell ',\alpha '[C'\mapsto 0]))}$, para${\displaystyle (\ell ,a,g,C',\ell ')\in E}$, de tal manera que${\displaystyle \gamma \models \alpha '}$y${\displaystyle \alpha '}$es un sucesor temporal de${\displaystyle \alpha }$.

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