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 la etiqueta de tiempo no debe ser decreciente , lo que intuitivamente significa que se reciben cartas. Por ejemplo, un sistema que recibe una palabra a través de una red puede asociar a cada letra el momento en que se recibe la letra. La condición no decreciente aquí significa que las cartas se reciben en el orden correcto.

Considere un ascensor. Lo que formalmente se llama una carta podría ser, de hecho, una 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 luego analizarse mediante un método formal para verificar si se cumple una propiedad tal que "cada vez que se llama al ascensor, llega en menos de tres minutos, suponiendo que nadie sostenga la puerta durante más de quince segundos". Una declaración como esta generalmente se expresa en lógica temporal métrica , una extensión de la lógica temporal lineal que permite expresar restricciones de tiempo.

Una palabra cronometrada se puede pasar a un modelo, como un autómata cronometrado , que decidirá, dadas las letras o acciones que ya ocurrieron, cuál es la siguiente acción que se debe realizar. En nuestro ejemplo, a qué piso debe ir el ascensor. Luego, un programa puede probar este autómata temporizado y verificar la propiedad mencionada anteriormente. Es decir, intentará generar un timed-word en el que la puerta nunca se mantiene abierta durante más de quince segundos, y en el que un usuario debe esperar más de tres minutos después de llamar al ascensor.

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

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