autómata híbrido

En teoría de autómatas , un autómata híbrido (plural: autómatas híbridos o autómatas híbridos ) es un modelo matemático para describir con precisión sistemas híbridos, por ejemplo sistemas en los que los procesos computacionales digitales interactúan con procesos físicos analógicos. Un autómata híbrido es una máquina de estados finitos con un conjunto finito de variables continuas cuyos valores se describen mediante un conjunto de ecuaciones diferenciales ordinarias . Esta especificación combinada de comportamientos discretos y continuos permite modelar y analizar sistemas dinámicos que comprenden componentes tanto digitales como analógicos.

Ejemplos

Un ejemplo sencillo es un sistema de termostato de ambiente -calefactor en el que la temperatura de la habitación evoluciona según las leyes de la termodinámica y el estado del calentador (encendido/apagado); el termostato detecta la temperatura, realiza ciertos cálculos y enciende y apaga el calentador. En general, los autómatas híbridos se han utilizado para modelar y analizar una variedad de sistemas integrados , incluidos sistemas de control de vehículos, sistemas de control de tráfico aéreo , robots móviles y procesos de biología de sistemas .

Definicion formal

Un autómata híbrido Alur-Henzinger consta de los siguientes componentes: ^[1] ${\displaystyle H}$

• Un conjunto finito de variables con números reales. El número se llama dimensión de . Sea el conjunto de variables punteadas que representan primeras derivadas durante el cambio continuo, y sea el conjunto de variables primadas que representan valores al final del cambio discreto. ${\displaystyle X=\{x_{1},...,x_{n}\}}$ ${\displaystyle n}$ ${\displaystyle H}$ ${\displaystyle {\dot {X}}}$ ${\displaystyle \{{\dot {x}}_{1},...,{\dot {x}}_{n}\}}$ ${\displaystyle X'}$ ${\displaystyle \{x'_{1},...,x'_{n}\}}$
• Un multidígrafo finito . Los vértices en se llaman modos de control . Los bordes hacia adentro se llaman interruptores de control . ${\displaystyle (V,E)}$ ${\displaystyle V}$ ${\displaystyle E}$
• Tres funciones de etiquetado de vértices init , inv y flow que asignan a cada modo de control tres predicados. Cada condición inicial init es un predicado cuyas variables libres son de . Cada condición invariante inv es un predicado cuyas variables libres son de . Cada condición de flujo es un predicado cuyas variables libres son de . ${\displaystyle v\in V}$ ${\displaystyle (v)}$ ${\displaystyle X}$ ${\displaystyle (v)}$ ${\displaystyle X}$ ${\displaystyle (v)}$ ${\displaystyle X\cup {\dot {X}}}$

Entonces este es un multidígrafo etiquetado .

• Un salto de función de etiquetado de bordes que asigna a cada interruptor de control un predicado. Cada condición de salto es un predicado cuyas variables libres son de . ${\displaystyle e\in E}$ ${\displaystyle (e)}$ ${\displaystyle X\cup X'}$
• Un conjunto finito de eventos y un evento de función de etiquetado de bordes : que asigna a cada interruptor de control un evento. ${\displaystyle \Sigma }$ ${\displaystyle E\rightarrow \Sigma }$

Modelos relacionados

Los autómatas híbridos vienen en varios tipos: el autómata híbrido Alur-Henzinger es un modelo popular; Fue desarrollado principalmente para el análisis algorítmico de la verificación de modelos de sistemas híbridos . La herramienta de verificación de modelos HyTech se basa en este modelo. Más recientemente se ha desarrollado el modelo de Autómata Híbrido de Entrada/Salida . Este modelo permite el modelado compositivo y el análisis de sistemas híbridos. Otro formalismo, que es útil para modelar implementaciones de autómatas híbridos, es el autómata híbrido lineal perezoso .

Subclase decidible de autómatas híbridos.

Dada la expresividad de los autómatas híbridos, no sorprende que las cuestiones simples de accesibilidad sean indecidibles para los autómatas híbridos generales. De hecho, una reducción sencilla de las máquinas contadoras a autómatas híbridos de tres variables (dos variables para almacenar los valores de los contadores y una para restringir el gasto de una unidad de tiempo por ubicación) demuestra la indecidibilidad del problema de accesibilidad para los autómatas híbridos. Una subclase de autómatas híbridos son los autómatas cronometrados ^[2] donde todas las variables crecen a un ritmo uniforme (es decir, todas las variables continuas tienen derivada 1). Estas variables restringidas pueden actuar como variables de temporizador, llamadas relojes, y permitir el modelado de sistemas en tiempo real. Otras subclases decidibles notables incluyen autómatas híbridos rectangulares inicializados, ^[3] sistemas unidimensionales de derivados constantes por partes (PCD), ^[4] autómatas temporizados con precio, ^[5] y sistemas multimodo de velocidad constante. ^[6]

Ver también

• Autómata cronometrado y autómata de señales , dos tipos de autómatas híbridos

Referencias

1. Henzinger, TA "La teoría de los autómatas híbridos". Actas del undécimo simposio anual del IEEE sobre lógica en informática (LICS), páginas 278-292, 1996.
2. Alur, R. y Dill, DL "Una teoría de los autómatas cronometrados". Ciencias de la Computación Teórica (TCS), 126 (2), páginas 183-235, 1995.
3. Henzinger, Thomas A.; Kopke, Peter W.; Puri, Anuj; Varaiya, Pravin (1 de agosto de 1998). "¿Qué es decidible acerca de los autómatas híbridos?". Revista de Ciencias de la Computación y de Sistemas . 57 (1): 94-124. doi :10.1006/jcss.1998.1581. hdl : 1813/7198 . ISSN  0022-0000.
4. Asarin, Eugenio; Schneider, Gerardo; Yovine, Sergio (2001), "Sobre la capacidad de decisión del problema de accesibilidad para inclusiones diferenciales planas", Sistemas híbridos: computación y control , Springer Berlin Heidelberg, págs. 89-104, CiteSeerX 10.1.1.23.8172 , doi :10.1007/3 -540-45351-2_11, ISBN  9783540418665
5. Behrmann, Gerd; Larsen, Kim G.; Rasmussen, Jacob I. (2005), "Autómatas cronometrados con precio: algoritmos y aplicaciones", Métodos formales para componentes y objetos , Springer Berlin Heidelberg, págs. 162–182, CiteSeerX 10.1.1.106.7115 , doi :10.1007/11561163_8, ISBN  9783540291312
6. Alur, Rajeev; Trivedi, Ashutosh; Wojtczak, Dominik (17 de abril de 2012). Programación óptima para sistemas multimodo de velocidad constante . ACM. págs. 75–84. CiteSeerX 10.1.1.299.946 . doi :10.1145/2185632.2185647. ISBN  9781450312202. S2CID  14587340.

Otras lecturas

• Rajeev Alur , Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis y Sergio Yovine El análisis algorítmico de sistemas híbridos . Informática teórica, volumen 138 (1), páginas 3 a 34, 1995.
• Nancy Lynch , Roberto Segala, Frits Vaandrager, Autómatas de E/S híbridas . Información y Computación, volumen 185 (1), páginas 103–157, 2003.