En la teoría de los autómatas , un autómata temporizado es un autómata finito ampliado con un conjunto finito de relojes de valor real. Durante una ejecución de un autómata temporizado, los valores del 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 inhabilitar 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 cronometrados se pueden utilizar para modelar y analizar el comportamiento temporal de los sistemas informáticos, por ejemplo, sistemas o redes en tiempo real. Los métodos para comprobar las propiedades de seguridad y vitalidad se han desarrollado y estudiado intensamente durante los últimos 20 años.
Se ha demostrado que el problema de la accesibilidad del estado para los autómatas temporizados es decidible, [1] lo que lo convierte en una subclase interesante de autómatas híbridos. Las extensiones se han estudiado extensamente, entre ellas cronómetros, tareas en tiempo real, funciones de costos y 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 son cada vez más maduras, pero siguen siendo todas herramientas de investigación académica.
Ejemplo
Antes de definir formalmente qué es un autómata temporizado, se dan algunos ejemplos.
Considere el idioma de palabras cronometradas sobre el alfabeto unario tal que hay un durante la primera unidad de tiempo, y hay menos de una unidad de tiempo entre dos sucesivas . El autómata cronometrado que reconoce este idioma, que se muestra cerca, usa un solo reloj , que nunca debería ser igual a uno. Este reloj cuenta el tiempo desde el inicio de la ejecución si no fueron emitidos, o desde el último emitido de otra manera. Significa que cada vez que un se emite, este reloj se pone a cero.
Considere el idioma de palabras cronometradas sobre el alfabeto binario tal que cada es seguido por un en la próxima unidad de tiempo. El autómata cronometrado que reconoce este lenguaje, fotografiado cerca, recuerda si hubo un que no fue seguido por un o no. Si no es el caso, acepta la ejecución, en caso contrario la rechaza. Además, cuando existe taltiene reloj que recuerdan el tiempo transcurrido desde la primera fue emitido. En este caso, un No se puede emitir si el reloj es al menos igual a uno y, por lo tanto, la ejecución falla.
Definicion formal
Autómata temporizado
Formalmente, un autómata temporizado es una tupla que consta de los siguientes componentes:
- es un conjunto finito llamado alfabeto o acciones de.
- es un conjunto finito . Los elementos dese llaman las ubicaciones o estados de.
- es el conjunto de ubicaciones de inicio.
- es un conjunto finito llamado los relojes de.
- es el conjunto de ubicaciones de aceptación.
- es un conjunto de aristas, llamadas transiciones de, dónde
- es el conjunto de restricciones de reloj que involucran relojes de, y
- es el conjunto de poder de.
Un borde de es una transición de ubicaciones a con accion , Guardia y el reloj se reinicia .
Estado extendido
Un par con una ubicación y una valoración de reloj se llama estado extendido o estado .
Tenga en cuenta que la palabra estado es, por tanto, ambigua, ya que, dependiendo del autor, puede significar un par o un elemento de . En aras de la claridad, este artículo utilizará el término ubicación para el elemento dey el término ubicación extendida para parejas.
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". Eso significa que, dado un estado y un sufijo de la palabra a leer, el resto de la carrera está totalmente determinado. Así, la palabra "finito" en el nombre de "autómatas finitos". Sin embargo, como se explica en la sección "ejecutar" a continuación, para reanudar, los relojes se utilizan para determinar qué transiciones se pueden tomar. Así, para conocer el estado del autómata, debes saber en qué ubicación te encuentras y la valoración del reloj.
Correr
Dada una palabra cronometrada con , una secuencia creciente de número no negativo, y un autómata temporizado como arriba, una ejecución es una secuencia de la forma satisfaciendo la siguiente restricción:
- (inicialización)
- (consecución), para todos , existe una ventaja en de la forma tal que:
- asumimos que Pasaron las unidades de tiempo, y en este momento, el guardia está satisfecho. Es decir satisface ,
- la nueva valoración del reloj corresponde a , en el cual unidades de tiempo pasaron y en las que los relojes de donde reiniciar. Formalmente,.
La noción de aceptación de ejecución se define como en autómatas finitos para palabras finitas y como en autómatas Büchi para palabras infinitas. Es decir, si es finito de longitud , entonces la carrera se acepta si . Si la palabra es infinita, entonces la carrera se acepta si y solo si existe un número infinito de posiciones tal que .
Autómata temporizado determinista
Como en el caso de los autómatas finitos y Büchi, un autómata temporizado puede ser determinista o no determinista. Intuitivamente, ser determinista tiene el mismo significado en cada uno de esos casos. Significa que el conjunto de ubicaciones de inicio es un singleton y que, dado un estadoy una carta , solo hay un estado posible que se puede alcanzar desde leyendo . Sin embargo, en el caso del autómata temporizado, la definición formal es un poco más compleja. Formalmente, un autómata temporizado es determinista si:
- 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 .
Propiedad de cierre
La clase de lenguajes reconocidos por los autómatas temporizados no deterministas es:
Problemas y su complejidad
Se da ahora la complejidad computacional de algunos problemas relacionados con los autómatas temporizados.
El problema del vacío del autómata temporizado se puede resolver construyendo un autómata de región y comprobando si acepta el lenguaje vacío. Este problema está completo en PSPACE . [1] : 207
El problema de universalidad del autómata temporizado 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 cronometrado.
Ver también
- Autómata temporizado alterno : una extensión de autómata temporizado con transiciones universales.
Notas
- ↑ a b Rajeev Alur, David L. Dill. 1994 Una teoría de los autómatas cronometrados . En Informática Teórica, vol. 126, 183–235, págs. 194–1955
- ^ Aplicaciones modernas de autómatas, página 118
- ^ a b Lasota, SƗawomir; Walukiewicz, Igor (2008). "Autómatas temporizados alternos". Transacciones ACM en lógica computacional . 9 (2): 1–26. arXiv : cs / 0512031 . doi : 10.1145 / 1342991.1342994 .