Autómata híbrido

En la teoría de los 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 en los que los procesos computacionales digitales interactúan con los 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 calefacción- termostato de habitación donde 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 que incluyen sistemas de control de vehículos, sistemas de control de tráfico aéreo , robots móviles y procesos de biología de sistemas .

Definición formal

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

• Un conjunto finito ${\displaystyle X=\{x_{1},...,x_{n}\}}$de variables numeradas reales. El número${\displaystyle n}$se llama la dimensión de${\displaystyle H}$. Dejar${\displaystyle {\dot {X}}}$ ser el set ${\displaystyle \{{\dot {x}}_{1},...,{\dot {x}}_{n}\}}$ de variables punteadas que representan las primeras derivadas durante el cambio continuo, y dejemos ${\displaystyle X'}$ ser el set ${\displaystyle \{x'_{1},...,x'_{n}\}}$ de variables primarias que representan valores al final del cambio discreto.
• Un multidigráfico finito ${\displaystyle (V,E)}$. Los vértices en${\displaystyle V}$se denominan modos de control . Los bordes en${\displaystyle E}$se llaman interruptores de control .
• Tres funciones de etiquetado de vértices init , inv y flow que se asignan a cada modo de control${\displaystyle v\in V}$tres predicados. Cada condición inicial init${\displaystyle (v)}$ es un predicado cuyas variables libres son de ${\displaystyle X}$. Cada condición invariante inv${\displaystyle (v)}$ es un predicado cuyas variables libres son de ${\displaystyle X}$. Cada flujo de condición de flujo${\displaystyle (v)}$ es un predicado cuyas variables libres son de ${\displaystyle X\cup {\dot {X}}}$.

Así que este es un multidígrafo etiquetado .

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

Modelos relacionados

Los autómatas híbridos vienen en varios sabores: 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. El modelo Hybrid Input / Output Automaton se ha desarrollado más recientemente. Este modelo permite el modelado composicional 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 es sorprendente que las preguntas simples de accesibilidad sean indecidibles para los autómatas híbridos generales. De hecho, una reducción directa de Counter machine a tres variables de autómatas híbridos (dos variables para almacenar valores de contador y una para restringir el gasto de una unidad de tiempo por ubicación) demuestra la indecidibilidad del problema de accesibilidad de los autómatas híbridos. Una subclase de autómatas híbridos son los autómatas cronometrados ^[2]donde todas las variables crecen con una tasa 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 derivadas constantes a trozos (PCD), ^[4] autómatas temporizados con precio, ^[5] y sistemas multimodo de tasa constante. ^[6]

Ver también

• Autómata temporizado y autómata de señal , 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 ciencias de la computación (LICS), páginas 278-292, 1996.
2. Alur, R. y Dill, DL "Una teoría de los autómatas cronometrados". Theoretical Computer Science (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 sobre los autómatas híbridos?". Revista de Ciencias de la Computación y Sistemas . 57 (1): 94-124. doi : 10.1006 / jcss.1998.1581 . hdl : 1813/7198 . ISSN  0022-0000 .
4. Asarin, Eugene; Schneider, Gerardo; Yovine, Sergio (2001), "On the Decidability of the Alcanbility Problem for Planar Differential Inclusions", Hybrid Systems: Computation and 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), "Priced Timed Automata: Algorithms and Applications", 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 tasa constante . ACM. págs. 75–84. CiteSeerX 10.1.1.299.946 . doi : 10.1145 / 2185632.2185647 . ISBN  9781450312202.

Lectura adicional

• 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 . Theoretical Computer Science, volumen 138 (1), páginas 3–34, 1995.
• Nancy Lynch , Roberto Segala, Frits Vaandrager, Autómatas de E / S híbridos . Information and Computation, volumen 185 (1), páginas 103-157, 2003.