Palabra cronometrada

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

Un lenguaje cronometradoes un conjunto de palabras cronometradas.

Consideremos un ascensor. Lo que formalmente se denomina letra podría ser, de hecho, información como «alguien pulsó el botón en el segundo piso» o «las puertas se abrieron en el tercer piso». En este caso, una palabra temporizada es una secuencia de acciones realizadas por el ascensor y sus usuarios, con marcas de tiempo para recordar dichas acciones. La palabra temporizada puede analizarse mediante métodos formales para comprobar si se cumple una propiedad como «cada vez que se llama al ascensor, llega en menos de tres minutos, suponiendo que nadie haya sujetado la puerta durante más de quince segundos». Una afirmación como esta se suele expresar en lógica temporal métrica , una extensión de la lógica temporal lineal que permite expresar restricciones de tiempo.

Se puede pasar una palabra temporizada a un modelo, como un autómata temporizado , que decidirá, en función de las letras o acciones ya realizadas, cuál es la siguiente acción a ejecutar. En nuestro ejemplo, a qué piso debe ir el ascensor. A continuación, un programa puede probar este autómata temporizado y comprobar la propiedad mencionada. Es decir, intentará generar una palabra temporizada en la que la puerta nunca permanezca abierta durante más de quince segundos y en la que el usuario deba 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.${\displaystyle w=(a_{0},t_{0})(a_{1},t_{1})\dots }$con${\displaystyle a_{i}\in A}$,${\displaystyle t_{i}\in \mathbb {R} _{+}}$con${\displaystyle t_{i}\leq t_{i+1}}$para cada entero${\displaystyle i}$.

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

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

• Alur, Rajeev ; Dill, David (1994). "Una teoría de autómatas temporizados" . Theoretical Computer Science . 126 (2): 190. doi : 10.1016/0304-3975(94)90010-8 .