Autómata temporizado

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

• ${\displaystyle \Sigma }$es un conjunto finito llamado alfabeto o acciones de${\displaystyle {\mathcal {A}}}$.
• ${\displaystyle L}$es un conjunto finito . Los elementos de${\displaystyle L}$se denominan ubicaciones o estados de${\displaystyle {\mathcal {A}}}$.
• ${\displaystyle L_{0}\subseteteq 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${\displaystyle {\mathcal {A}}}$, dónde
  • ${\displaystyle {\mathcal {B}}(C)}$es el conjunto de restricciones de reloj que involucran relojes de${\displaystyle C}$, y
  • ${\displaystyle {\mathcal {P}}(C)}$es el conjunto potencia de${\displaystyle C}$.

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

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

Nótese que la palabra estado es, por lo tanto, ambigua, ya que, dependiendo del autor, puede significar tanto un par como un elemento de${\displaystyle L}$. Para mayor claridad, este artículo utilizará el término ubicación para referirse al elemento de${\displaystyle L}$y el término ubicación extendida para pares.

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 se describe completamente 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 el sufijo de la palabra a leer, el resto de la ejecución está totalmente determinado. De ahí el término "finito" en "autómata finito". Sin embargo, como se explica en la sección "ejecución" más adelante, se utilizan relojes para determinar qué transiciones se pueden realizar. Por lo tanto, para conocer el estado del autómata, es necesario conocer tanto la ubicación como la valoración del reloj.

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

• (inicialización)${\displaystyle \ell _{0}\in L_{0}}$
• (procedimiento), para todos${\displaystyle i\geq 1}$, existe una arista en${\displaystyle E}$de la forma${\displaystyle \langle \ell _{i-1},\sigma _{i},g_{i},r_{i},\ell _{i}\rangle }$de tal manera que:
  • asumimos que${\displaystyle t_{i}-t_{i-1}}$Transcurrieron unidades de tiempo y, en este momento, el guardia está satisfecho. Es decir,${\displaystyle \nu _{i-1}+t_{i}-t_{i-1}}$Satisface${\displaystyle g_{i}}$,
  • la nueva valoración del reloj${\displaystyle \nu _{i}}$corresponde a${\displaystyle \nu _{i-1}}$, en el cual${\displaystyle t_{i}-t_{i-1}}$unidades de tiempo transcurridas y en las que los relojes de${\displaystyle r_{i}}$donde se reinicia. Formalmente,${\displaystyle \nu _{i}=(\nu _{i-1}+t_{i}-t_{i-1})[r_{i}\rightarrow 0]}$.

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

Al igual que en el caso de los autómatas finitos y de Büchi, un autómata temporizado puede ser determinista o no determinista. Intuitivamente, ser determinista tiene el mismo significado en ambos casos. Significa que el conjunto de ubicaciones iniciales es un conjunto único y que, dado un estado${\displaystyle s}$y una carta${\displaystyle a}$, solo hay un estado posible al que se puede llegar desde${\displaystyle s}$leyendo${\displaystyle a}$Sin embargo, en el caso de un autómata temporizado, la definición formal es un poco más compleja. Formalmente, un autómata temporizado es determinista si:

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