Autômato híbrido
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:[1]
- 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.
Referências
- ↑ 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.
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.
![]() | Este artigo sobre computação é um esboço. Você pode ajudar a Wikipédia expandindo-o.
|