Na teoria dos autômatos, um autômato híbrido é um modelo matemático para descrever precisamente sistemas onde processos computacionais digitais interagem com processos físicos analógicos. Um autômato híbrido é uma máquina de estados finitos com um conjunto finito de variáveis contínuas, cujos valores são descritos por um conjunto de equações diferenciais comuns. Esta especificação combinada de comportamentos discretos e contínuos permite que sistemas dinâmicos que compreendem dois componentes digitais e analógicos a serem modelados e analisados.
Exemplos Um exemplo simples é o sistema sala-termostato-aquecedor, onde a temperatura da sala evolui de acordo com duas leis, as da termodinâmica, e do estado do aquecedor (ligado / desligado); o termostato julga a temperatura, executa computações precisas e modifica o aquecedor para ligado e desligado. Em geral, os autômatos híbridos têm sido usados para modelar e analisar uma grande variedade de sistemas embarcados, incluindo sistemas de controle de veículos, sistemas de controle de tráfego aéreo, robôs móveis, e processos de sistemas da biologia..
Definição Formal
Um autômato híbrido Alur-Henzinger H compreende os seguintes componentes:Henzinger, T.A. "The Theory of Hybrid Automata". Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS), pages 278-292, 1996.
Um conjunto finito de variáveis de números reais. O número é chamado de dimensão de . Faça ser o conjunto de variáveis pontuais que representam as primeiras derivadas durante a transformação contínua, e faça ser o conjunto de variáveis preparadas que representam valores na conclusão de transformação discreta. Um multigrafo finito direcionado . Os vértices em são chamados de modos de controle. As arestas em são chamadas de interruptores de controle. Três funções de rotulagem de vértices init, inv, and flow que atribuem a cada modo de controle três predicados. Cada condição inicial init é um predicado cujas variáveis livres são de . Cada condição invariante inv é um predicado cujas variáveis livres são de . Cada fluxo condição de fluxo flow é um predicado cujas variáveis livres são de . Uma função de rotulagem de arestas jump ,que atribui a cada interruptor de controle um predicado. Cada condição de salto jump é um predicado cujas variáveis livres são de . Um conjunto finito de eventos , e uma função de rotulagem de arestas event: que atribui a cada interruptor de controle um evento.
Modelos Relacionados Autômatos híbridos ocorrem de várias maneiras: o automato híbrido Alur-Henzinger é um modelo popular, que foi desenvolvido primeiramente para a análise algorítmica do modelo de verificação de sistemas híbridos. A ferramenta de verificação modelo HyTech é baseado nesse modelo. O modelo Autômato Entrada/Saída Híbrido foi desenvolvida mais recentemente. Este modelo permite a modelagem composicional e a análise de sistemas híbridos. Outro formalismo que é útil para implementações do modelo dos autômatos híbridos é o autômato híbrido preguiçoso linear.
Bibliografia Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and Sergio Yovine The algorithmic analysis of hybrid systems. Theoretical Computer Science, volume 138(1), pages 3–34, 1995.
Nancy Lynch, Roberto Segala, Frits Vaandrager, Hybrid I/O Automata. Information and Computation, volume 185(1), pages 103–157, 2003.
Categoria:Ciência da computação