Reloj (verificación de modelo)

Una valoración o interpretación de un reloj ^{[ 1 ] : 193}${\displaystyle \nu }$encima${\displaystyle X=\{x_{1},\dots ,x_{n}\}}$generalmente se define como una función de${\displaystyle X}$al conjunto de los números reales no negativos. De forma equivalente, una valoración puede considerarse como un punto en${\displaystyle \mathbb {R} _{\geq 0}^{n}}$.

La tarea inicial${\displaystyle \nu _{0}}$es la función constante que envía cada reloj a 0. Intuitivamente, representa el tiempo inicial del programa, donde todos los relojes se inicializan simultáneamente.

Se me asignó un reloj${\displaystyle \nu }$y un verdadero${\displaystyle t\geq 0}$,${\displaystyle \nu +t}$indica la asignación de reloj que envía cada reloj${\displaystyle x\in C}$a${\displaystyle \nu (x)+t}$Intuitivamente, representa la valoración${\displaystyle \nu }$después de lo cual${\displaystyle t}$unidades de tiempo transcurridas.

Dado un subconjunto${\displaystyle r\subseteq C}$de relojes,${\displaystyle \nu [r\rightarrow 0]}$denota la asignación similar a${\displaystyle \nu }$en el que los relojes de${\displaystyle r}$se reinician. Formalmente,${\displaystyle \nu [r\rightarrow 0]}$envía cada reloj${\displaystyle x\in r}$a 0 y cada reloj${\displaystyle x\not \in r}$a${\displaystyle \nu (x)}$.

El programa UPPAAL introduce la noción de relojes inactivos . ^{[ 2 ]} Un reloj está inactivo en algún momento si no hay ningún futuro posible en el que se compruebe el valor del reloj sin reiniciarlo primero. En nuestro ejemplo anterior, el reloj${\displaystyle c_{i}}$Se considera inactivo cuando el ascensor llega al piso${\displaystyle i}$y permanece inactivo hasta que alguien llama al ascensor en el piso${\displaystyle i}$.

Al permitir relojes inactivos, una valoración puede asociar un reloj${\displaystyle x}$a algún valor especial${\displaystyle \bot }$para indicar que está inactivo. Si${\displaystyle \nu (x)=\bot }$entonces${\displaystyle (\nu +t)(x)}$también es igual a${\displaystyle \bot }$.

Dependiendo del contexto, una restricción de reloj atómico también puede tener la forma${\displaystyle x_{i}\sim x_{j}+c}$. Dicha restricción se denomina restricción diagonal, porque${\displaystyle x_{1}=x_{2}+c}$define una línea diagonal en${\displaystyle \mathbb {R} _{\geq 0}^{2}}$.

Permitir restricciones diagonales puede reducir el tamaño de una fórmula o de un autómata utilizado para describir un sistema. Sin embargo, la complejidad del algoritmo puede aumentar al permitir restricciones diagonales. En la mayoría de los sistemas que utilizan relojes, permitir restricciones diagonales no aumenta la expresividad de la lógica. A continuación, explicamos cómo codificar dichas restricciones con variables booleanas y restricciones no diagonales.

Una restricción diagonal${\displaystyle x_{i}\sim x_{j}+c}$puede simularse utilizando restricciones no diagonales de la siguiente manera. Cuando${\displaystyle x_{j}}$se reinicia, compruebe si${\displaystyle x_{i}\sim c}$Se cumple o no. Guarda esta información en una variable booleana.${\displaystyle b_{i,j,c}}$y reemplazar${\displaystyle x_{i}\sim x_{j}+c}$por esta variable. Cuando${\displaystyle x_{i}}$se reinicia, se establece${\displaystyle b_{i,j,c}}$verdadero si${\displaystyle \sim }$es < o ≤ o si${\displaystyle \sim }$es = y${\displaystyle c=0}$.

La forma de codificar una variable booleana depende del sistema que utiliza el reloj. Por ejemplo, UPPAAL admite variables booleanas directamente. Los autómatas temporizados y los autómatas de señales pueden codificar un valor booleano en sus ubicaciones. En la lógica temporal de reloj sobre palabras temporizadas, la variable booleana puede codificarse utilizando un nuevo reloj.${\displaystyle x_{i,j,c}}$, cuyo valor es 0 si y solo si${\displaystyle b_{i,j,c}}$es falso. Es decir,${\displaystyle x_{i,j,c}}$se reinicia siempre que${\displaystyle x_{i,j,c}}$Se supone que es falso. En la lógica temporal proposicional cronometrada , la fórmula${\displaystyle x_{i}.\phi }$, que se reinician${\displaystyle x_{i}}$y luego evalúa${\displaystyle \phi }$, puede ser reemplazado por la fórmula${\displaystyle x_{i}.((x_{i}\sim x_{j}+c\implies \phi _{\top })\land (\neg x_{i}\sim x_{j}+c\implies \phi \bot ))}$, dónde${\displaystyle \phi _{\top }}$y${\displaystyle \phi _{\bot }}$son copias de las fórmulas${\displaystyle \phi }$, dónde${\displaystyle x_{i}\sim x_{j}+c}$se reemplazan por la constante verdadera y falsa respectivamente.

Una restricción de reloj define un conjunto de valoraciones. En la literatura se consideran dos tipos de dichos conjuntos.

Una zona es un conjunto no vacío de valoraciones que satisface una restricción de reloj. Las zonas y las restricciones de reloj se implementan utilizando la matriz de límites de diferencia .

Dado un modelo ${\displaystyle M}$, utiliza un número finito de constantes en sus restricciones de reloj. Sea${\displaystyle K}$sea ​​la mayor constante utilizada. Una región es una zona no vacía en la que no hay ninguna restricción mayor que${\displaystyle K}$se utilizan y, además, de tal manera que sea mínimo para la inclusión.