Reloj (verificación de modelos)

En la verificación de modelos , un subcampo de la informática , un reloj es un objeto matemático utilizado para modelar el tiempo. Más precisamente, un reloj mide cuánto tiempo ha pasado desde que ocurre un evento particular; en este sentido, un reloj es más precisamente una abstracción de un cronómetro . En un modelo de algún programa particular, el valor del reloj puede ser el tiempo desde que se inició el programa o el tiempo desde que ocurrió un evento particular en el programa. Esos relojes se utilizan en la definición de autómata temporizado , autómata de señal , lógica temporal proposicional temporizada y lógica temporal de reloj. También se utilizan en programas como UPPAAL que implementan autómatas temporizados. ^[1]

Generalmente, el modelo de un sistema utiliza muchos relojes. Esos múltiples relojes son necesarios para realizar un seguimiento de un número limitado de eventos. Todos esos relojes están sincronizados. Eso significa que la diferencia de valor entre dos relojes fijos es constante hasta que uno de ellos se reinicia. En el lenguaje de la electrónica, significa que la fluctuación del reloj es nula.

Ejemplo

Supongamos que queremos modelar un ascensor en un edificio de diez pisos. Nuestro modelo puede tener relojes , de modo que el valor del reloj sea el tiempo que alguien tuvo que esperar el ascensor en el piso . Este reloj se pone en marcha cuando alguien llama al ascensor en el piso (y el ascensor no había sido llamado ya en este piso desde la última vez que visitó ese piso). Este reloj se puede apagar cuando el ascensor llega al piso . En este ejemplo, en realidad necesitamos diez relojes distintos porque necesitamos rastrear diez eventos independientes. Se puede utilizar otro reloj para comprobar cuánto tiempo pasó un ascensor en un piso en particular. ${\displaystyle n}$ ${\displaystyle c_{0},\dots ,c_{9}}$ ${\displaystyle c_{i}}$ ${\displaystyle i}$ ${\displaystyle i}$ ${\displaystyle i}$ ${\displaystyle s}$

Un modelo de este ascensor puede entonces utilizar esos relojes para comprobar si el programa del ascensor satisface propiedades como "suponiendo que el ascensor no se mantiene en un piso durante más de quince segundos, entonces nadie tiene que esperar al ascensor durante más de tres minutos". Para comprobar si esta afirmación es cierta, basta con comprobar que, en cada ejecución del modelo en la que el reloj sea siempre menor de quince segundos, cada reloj se apague antes de que llegue a los tres minutos. ${\displaystyle s}$ ${\displaystyle c_{i}}$

Definición

Formalmente, un conjunto de relojes es simplemente un conjunto finito ^{[1] : 191} . Cada elemento de un conjunto de relojes se denomina reloj. Intuitivamente, un reloj es similar a una variable en lógica de primer orden , es un elemento que puede usarse en una fórmula lógica y que puede tomar varios valores diferentes. ${\displaystyle X}$

Valoraciones de relojes

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

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

Dada una asignación de reloj y un valor real , denota la asignación de reloj que envía cada reloj a . Intuitivamente, representa la valoración después de la cual transcurrieron las unidades de tiempo. ${\displaystyle \nu }$ ${\displaystyle t\geq 0}$ ${\displaystyle \nu +t}$ ${\displaystyle x\in C}$ ${\displaystyle \nu (x)+t}$ ${\displaystyle \nu }$ ${\displaystyle t}$

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

Relojes inactivos

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

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

Restricción de reloj

Una restricción de reloj atómico es simplemente un término de la forma , donde es un reloj, es un operador de comparación, como <, ≤, = ≥ o >, y es una constante integral. En nuestro ejemplo anterior, podemos usar las restricciones de reloj atómico para indicar que la persona en el piso esperó menos de tres minutos y para indicar que el ascensor permaneció en algún piso durante más de quince segundos. Una valoración satisface una valoración de reloj atómico si y solo si . ${\displaystyle x\sim c}$ ${\displaystyle x}$ ${\displaystyle \sim }$ ${\displaystyle c\in \mathbb {N} }$ ${\displaystyle c_{i}\leq 180}$ ${\displaystyle i}$ ${\displaystyle s>15}$ ${\displaystyle \nu }$ ${\displaystyle x\sim c}$ ${\displaystyle \nu (x)\sim c}$

Una restricción de reloj es una conjunción finita de una restricción de reloj atómico o es la constante "verdadera" (que puede considerarse como la conjunción vacía). Una valoración satisface una restricción de reloj si satisface cada restricción de reloj atómico . ${\displaystyle \nu }$ ${\displaystyle \bigwedge _{i=1}^{n}x_{i}\sim _{i}c_{i}}$ ${\displaystyle x_{i}\sim _{i}c_{i}}$

Restricción diagonal

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

Permitir restricciones diagonales puede permitir 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 cuando se permiten restricciones diagonales. En la mayoría de los sistemas que utilizan relojes, permitir la restricción diagonal no aumenta la expresividad de la lógica. Ahora explicamos cómo codificar dicha restricción con una variable booleana y una restricción no diagonal.

Una restricción diagonal se puede simular utilizando una restricción no diagonal de la siguiente manera. Cuando se restablece, se verifica si se cumple o no. Se recupera esta información en una variable booleana y se reemplaza por esta variable. Cuando se restablece, se establece como verdadero si es < o ≤ o si es = y . ${\displaystyle x_{i}\sim x_{j}+c}$ ${\displaystyle x_{j}}$ ${\displaystyle x_{i}\sim c}$ ${\displaystyle b_{i,j,c}}$ ${\displaystyle x_{i}\sim x_{j}+c}$ ${\displaystyle x_{i}}$ ${\displaystyle b_{i,j,c}}$ ${\displaystyle \sim }$ ${\displaystyle \sim }$ ${\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 , cuyo valor es 0 si y solo si es falso. Es decir, se reinicia siempre que se suponga que es falso. En la lógica temporal proposicional temporizada , la fórmula , que reinicia y luego evalúa , puede reemplazarse por la fórmula , donde y son copias de las fórmulas , donde se reemplazan por la constante verdadero y falso respectivamente. ${\displaystyle x_{i,j,c}}$ ${\displaystyle b_{i,j,c}}$ ${\displaystyle x_{i,j,c}}$ ${\displaystyle x_{i,j,c}}$ ${\displaystyle x_{i}.\phi }$ ${\displaystyle x_{i}}$ ${\displaystyle \phi }$ ${\displaystyle x_{i}.((x_{i}\sim x_{j}+c\implies \phi _{\top })\land (\neg x_{i}\sim x_{j}+c\implies \phi \bot ))}$ ${\displaystyle \phi _{\top }}$ ${\displaystyle \phi _{\bot }}$ ${\displaystyle \phi }$ ${\displaystyle x_{i}\sim x_{j}+c}$

Conjuntos definidos por restricciones de reloj

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

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

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

Véase también

• Autómata cronometrado
• Autómata de señales
• Lógica temporal del reloj
• Lógica temporal proposicional cronometrada

Notas

1. 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 .
2. Behrmann, Gerd; David, Alexandre; Larsen, Kim G (28 de noviembre de 2006). "Un tutorial sobre Uppaal 4.0" (PDF) : 28. {{cite journal}}: Requiere citar revista |journal=( ayuda )