Palabra cronometrada

En la verificación de modelos , un subcampo de la informática , una palabra cronometrada es una extensión de la noción de palabras, en un lenguaje formal , en el que cada letra está asociada con una etiqueta de tiempo positiva. La secuencia de etiquetas de tiempo debe ser no decreciente , lo que intuitivamente significa que se reciben letras. Por ejemplo, un sistema que recibe una palabra a través de una red puede asociar a cada letra el momento en el que se recibe la letra. La condición no decreciente aquí significa que las letras se reciben en el orden correcto.

Un lenguaje cronometradoes un conjunto de palabras cronometradas.

Ejemplo

Consideremos un ascensor. Lo que formalmente se denomina una carta podría ser, de hecho, información como "alguien presionó el botón en el segundo piso" o "las puertas se abrieron en el tercer piso". En este caso, una palabra cronometrada es una secuencia de acciones realizadas por los ascensores y sus usuarios, con marcas de tiempo para recordar esas acciones. La palabra cronometrada puede entonces analizarse mediante métodos formales para verificar si se cumple una propiedad como "cada vez que se llama al ascensor, llega en menos de tres minutos suponiendo que nadie sostuvo la puerta durante más de quince segundos". Una afirmación como esta suele expresarse en lógica temporal métrica , una extensión de la lógica temporal lineal que permite la expresión de restricciones temporales.

Se puede pasar una palabra temporizada a un modelo, como un autómata temporizado , que decidirá, dadas las letras o acciones que ya han ocurrido, cuál es la siguiente acción que debe realizarse. En nuestro ejemplo, a qué piso debe ir el ascensor. Luego, un programa puede probar este autómata temporizado y comprobar la propiedad mencionada anteriormente. Es decir, intentará generar una palabra temporizada en la que la puerta nunca se mantenga abierta durante más de quince segundos, y en la que un usuario deba esperar más de tres minutos después de llamar al ascensor.

Definición

Dado un alfabeto A , una palabra cronometrada es una secuencia, finita o infinita con , con para cada entero . ${\displaystyle w=(a_{0},t_{0})(a_{1},t_{1})\dots }$ ${\displaystyle a_{i}\in A}$ ${\displaystyle t_{i}\in \mathbb {R} _{+}}$ ${\displaystyle t_{i}\leq t_{i+1}}$ ${\displaystyle i}$

Si la secuencia es infinita pero la secuencia de está acotada, entonces se dice que esta palabra es una palabra cronometrada por Zenón. ${\displaystyle (t_{0})(t_{1})\dots }$, ^[1] en referencia a las paradojas de Zenón , donde un número infinito de acciones ocurren en un tiempo finito.

La palabra ${\displaystyle \operatorname {untimed} (w)}$es la palabra sin sus marcas de tiempo, es decir, es . Dado un lenguaje cronometrado , es entonces el conjunto de para . ${\displaystyle w}$ ${\displaystyle a_{0}a_{1}\dots }$ ${\displaystyle L}$ ${\displaystyle \operatorname {untimed} (L)}$ ${\displaystyle \operatorname {untimed} (w)}$ ${\displaystyle w\in L}$

Referencias

1. Estévenart, Morgane (septiembre de 2015). "2". Verificación y síntesis de MITL mediante autómatas temporizados alternados (PhD). pág. 56.

• Alur, Rajeev ; Dill, David (1994). "Una teoría de autómatas temporizados". Ciencias Informáticas Teóricas . 126 (2): 190. doi : 10.1016/0304-3975(94)90010-8 .