Autómata cronometrado

En la teoría de autómatas , un autómata temporizado es un autómata finito ampliado con un conjunto finito de relojes de valor real. Durante la ejecución de un autómata temporizado, los valores de reloj aumentan todos con la misma velocidad. A lo largo de las transiciones del autómata, los valores de reloj se pueden comparar con números enteros. Estas comparaciones forman protecciones que pueden habilitar o deshabilitar las transiciones y, al hacerlo, restringen los posibles comportamientos del autómata. Además, los relojes se pueden reiniciar. Los autómatas temporizados son una subclase de un tipo de autómatas híbridos .

Los autómatas temporizados se pueden utilizar para modelar y analizar el comportamiento temporal de los sistemas informáticos, por ejemplo, sistemas o redes en tiempo real. Durante los últimos 20 años se han desarrollado y estudiado intensamente métodos para comprobar las propiedades de seguridad y vitalidad.

Se ha demostrado que el problema de alcanzabilidad de estados para autómatas cronometrados es decidible , ^[1] lo que hace de esta una interesante subclase de autómatas híbridos. Las extensiones se han estudiado ampliamente, entre ellas los cronómetros, las tareas en tiempo real, las funciones de costo y los juegos cronometrados. Existe una variedad de herramientas para ingresar y analizar autómatas cronometrados y extensiones, incluidos los verificadores de modelos UPPAAL , Kronos y el analizador de programabilidad TIMES. Estas herramientas se están volviendo cada vez más maduras, pero aún son todas herramientas de investigación académica.

Ejemplo

Antes de definir formalmente qué es un autómata cronometrado, se dan algunos ejemplos.

Consideremos el lenguaje de palabras cronometradas sobre el alfabeto unario de modo que hay un durante la primera unidad de tiempo, y hay menos de una unidad de tiempo entre dos sucesivos . Un autómata cronometrado que reconoce este lenguaje, representado al lado, utiliza un solo reloj , que nunca debe ser igual a uno. Este reloj cuenta el tiempo desde el inicio de la ejecución si no se emitieron , o desde la última emisión en caso contrario. Esto significa que cada vez que se emite un , este reloj se reinicia a cero. ${\displaystyle {\mathcal {L}}}$ ${\displaystyle w}$ ${\displaystyle \{a\}}$ ${\displaystyle a}$ ${\displaystyle a}$ ${\displaystyle x}$ ${\displaystyle a}$ ${\displaystyle a}$ ${\displaystyle a}$

Autómata cronometrado que acepta el lenguaje a* tal que se emite una letra en cada intervalo abierto de longitud uno.

Consideremos el lenguaje de palabras cronometradas sobre el alfabeto binario de modo que cada una de ellas sea seguida por una a en la siguiente unidad de tiempo. El autómata cronometrado que reconoce este lenguaje, representado en la imagen de al lado, recuerda si había o no una a que no fuera seguida por una . Si no es el caso, acepta la ejecución; de lo contrario, la rechaza. Además, cuando hay una tal , tiene un reloj que registra el tiempo transcurrido desde que se emitió la primera tal. En este caso, no se puede emitir una a si el reloj es al menos igual a uno, y por lo tanto la ejecución falla. ${\displaystyle {\mathcal {L}}}$ ${\displaystyle w}$ ${\displaystyle \{a,b\}}$ ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle a}$ ${\displaystyle b}$ ${\displaystyle a}$ ${\displaystyle x}$ ${\displaystyle a}$ ${\displaystyle b}$

Un autómata cronometrado que acepta palabras cronometradas sobre donde cada ocurrencia de es seguida menos de una unidad de tiempo después por una ocurrencia de . ${\displaystyle \{a,b\}}$ ${\displaystyle a}$ ${\displaystyle b}$

Definición formal

Autómata cronometrado

Formalmente, un autómata cronometrado es una tupla que consta de los siguientes componentes: ${\displaystyle {\mathcal {A}}=\langle \Sigma ,L,L_{0},C,F,E\rangle }$

• ${\displaystyle \Sigma }$es un conjunto finito llamado alfabeto o acciones de . ${\displaystyle {\mathcal {A}}}$
• ${\displaystyle L}$es un conjunto finito . Los elementos de se denominan ubicaciones o estados de . ${\displaystyle L}$ ${\displaystyle {\mathcal {A}}}$
• ${\displaystyle L_{0}\subseteq L}$ es el conjunto de ubicaciones de inicio.
• ${\displaystyle C}$es un conjunto finito llamado los relojes de . ${\displaystyle {\mathcal {A}}}$
• ${\displaystyle F\subseteq L}$es el conjunto de ubicaciones de aceptación.
• ${\displaystyle E\subseteq L\times \Sigma \times {\mathcal {B}}(C)\times {\mathcal {P}}(C)\times L}$es un conjunto de aristas, llamadas transiciones de , donde ${\displaystyle {\mathcal {A}}}$
  • ${\displaystyle {\mathcal {B}}(C)}$es el conjunto de restricciones de reloj que involucran los relojes de , y ${\displaystyle C}$
  • ${\displaystyle {\mathcal {P}}(C)}$es el conjunto potencia de . ${\displaystyle C}$

Un borde desde es una transición de ubicaciones a con acción , guardia y reinicios del reloj . ${\displaystyle (\ell ,\sigma ,g,r,\ell ')}$ ${\displaystyle E}$ ${\displaystyle \ell }$ ${\displaystyle \ell '}$ ${\displaystyle \sigma }$ ${\displaystyle g}$ ${\displaystyle r}$

Estado extendido

Un par con una ubicación y una valoración de reloj se denomina estado extendido o estado . ${\displaystyle \ell }$ ${\displaystyle \nu }$

Obsérvese que la palabra estado es, por lo tanto, ambigua, ya que, según el autor, puede significar un par o un elemento de . Para mayor claridad, en este artículo se utilizará el término ubicación para el elemento de y el término ubicación extendida para los pares. ${\displaystyle L}$ ${\displaystyle L}$

Aquí radica una de las mayores diferencias entre los autómatas temporizados y los autómatas finitos . En un autómata finito, en algún punto de la ejecución, el estado está completamente descrito por el número de letras leídas y por un número finito de valores posibles, que en realidad se denominan "estados". Esto significa que, dado un estado y un sufijo de la palabra a leer, el resto de la ejecución está totalmente determinado. De ahí la palabra "finito" en el nombre "autómatas finitos". Sin embargo, como se explica en la sección "ejecución" más adelante, para reanudar se utilizan relojes para determinar qué transiciones se pueden realizar. Por lo tanto, para conocer el estado del autómata, debe saber tanto en qué ubicación se encuentra como la valoración del reloj.

Correr

Dada una palabra cronometrada con , una secuencia creciente de números no negativos y un autómata cronometrado como el anterior, una ejecución es una secuencia de la forma que satisface la siguiente restricción: ${\displaystyle w=(\sigma _{1},t_{1}),(\sigma _{2},t_{2}),\dots ,}$ ${\displaystyle \sigma _{i}\in \Sigma }$ ${\displaystyle (t_{i})_{i}}$ ${\displaystyle {\mathcal {A}}}$ ${\displaystyle (\ell _{0},\nu _{0}){\xrightarrow[{t_{1}}]{\sigma _{1}}}(\ell _{1},\nu _{1})\dots }$

• (inicialización) ${\displaystyle \ell _{0}\in L_{0}}$
• (consecuencia), para todo , existe una arista en de la forma tal que: ${\displaystyle i\geq 1}$ ${\displaystyle E}$ ${\displaystyle \langle \ell _{i-1},\sigma _{i},g_{i},r_{i},\ell _{i}\rangle }$
  • Suponemos que han pasado unidades de tiempo y en ese momento el guardia está satisfecho, es decir satisface , ${\displaystyle t_{i}-t_{i-1}}$ ${\displaystyle \nu _{i-1}+t_{i}-t_{i-1}}$ ${\displaystyle g_{i}}$
  • La nueva valoración del reloj corresponde a , en la que transcurrieron unidades de tiempo y en la que se pusieron a cero los relojes de . Formalmente, . ${\displaystyle \nu _{i}}$ ${\displaystyle \nu _{i-1}}$ ${\displaystyle t_{i}-t_{i-1}}$ ${\displaystyle r_{i}}$ ${\displaystyle \nu _{i}=(\nu _{i-1}+t_{i}-t_{i-1})[r_{i}\rightarrow 0]}$

La noción de ejecución aceptable se define como en autómatas finitos para palabras finitas y como en autómatas de Büchi para palabras infinitas. Es decir, si es finito de longitud , entonces la ejecución es aceptable si . Si la palabra es infinita, entonces la ejecución es aceptable si y solo si existe un número infinito de posiciones tales que . ${\displaystyle w}$ ${\displaystyle n}$ ${\displaystyle \ell _{n}\in F}$ ${\displaystyle i}$ ${\displaystyle \ell _{i}\in F}$

Autómata cronometrado determinista

Al igual que en el caso de los autómatas finitos y de Büchi, un autómata cronometrado puede ser determinista o no determinista. Intuitivamente, ser determinista tiene el mismo significado en cada uno de esos casos. Significa que el conjunto de posiciones de inicio es un singleton y que, dado un estado y una letra , solo hay un estado posible al que se puede llegar leyendo . Sin embargo, en el caso de un autómata cronometrado la definición formal es ligeramente más compleja. Formalmente, un autómata cronometrado es determinista si: ${\displaystyle s}$ ${\displaystyle a}$ ${\displaystyle s}$ ${\displaystyle a}$

• ${\displaystyle L_{0}}$es un singleton
• para cada par de transiciones y , el conjunto de valoraciones de relojes que satisfacen es disjunto del conjunto de valoraciones de relojes que satisfacen . ${\displaystyle (\ell ,\sigma ,g,r,\ell ')}$ ${\displaystyle (\ell ,\sigma ,g',r',\ell '')}$ ${\displaystyle g}$ ${\displaystyle g'}$

Propiedad de cierre

La clase de lenguajes reconocidos por los autómatas temporizados no deterministas es:

• cerrado bajo unión, de hecho, la unión disjunta de dos autómatas temporizados reconoce la unión del lenguaje reconocido por esos autómatas.
• cerrado bajo intersección. ^[2]
• no cerrado bajo complemento. ^[3]

Los problemas y su complejidad

A continuación se describe la complejidad computacional de algunos problemas relacionados con autómatas cronometrados.

El problema del vacío para autómatas temporizados se puede resolver construyendo un autómata de región y comprobando si acepta el lenguaje vacío. Este problema es PSPACE-completo . ^{[1] : 207}

El problema de universalidad del autómata cronometrado no determinista es indecidible, y más precisamente Π1 1. Sin embargo, cuando el autómata contiene un solo reloj, la propiedad es decidible; sin embargo, no es recursiva primitiva . ^[3] Este problema consiste en decidir si cada palabra es aceptada por un autómata temporizado.

Véase también

• Autómata cronometrado alterno : una extensión del autómata cronometrado con transiciones universales.

Notas

1. Rajeev Alur, David L. Dill. 1994 Una teoría de autómatas temporizados. En Theoretical Computer Science , vol. 126, 183–235, págs. 194–1955
2. Aplicaciones modernas de los autómatas, página 118
3. Lasota, SƗawomir; Walukiewicz, Igor (2008). "Autómatas temporizados alternos". ACM Transactions on Computational Logic . 9 (2): 1–26. arXiv : cs/0512031 . doi :10.1145/1342991.1342994. S2CID  12319.