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 ${\displaystyle X=\{x_{1},...,x_{n}\}}$ de variáveis de números reais. O número ${\displaystyle n}$ é chamado de dimensão de ${\displaystyle H}$. Faça ${\displaystyle {\dot {X}}}$ ser o conjunto ${\displaystyle \{{\dot {x}}_{1},...,{\dot {x}}_{n}\}}$ de variáveis pontuais que representam as primeiras derivadas durante a transformação contínua, e faça ${\displaystyle X'}$ ser o conjunto ${\displaystyle \{x'_{1},...,x'_{n}\}}$ de variáveis preparadas que representam valores na conclusão de transformação discreta.
• Um multigrafo finito direcionado ${\displaystyle (V,E)}$. Os vértices em ${\displaystyle V}$ são chamados de modos de controle. As arestas em ${\displaystyle E}$ 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 ${\displaystyle v\in V}$ três predicados. Cada condição inicial init${\displaystyle (v)}$ é um predicado cujas variáveis livres são de ${\displaystyle X}$. Cada condição invariante inv${\displaystyle (v)}$ é um predicado cujas variáveis livres são de ${\displaystyle X}$. Cada fluxo condição de fluxo flow${\displaystyle (v)}$ é um predicado cujas variáveis livres são de ${\displaystyle X\cup X}$.
• Uma função de rotulagem de arestas jump ,que atribui a cada interruptor de controle ${\displaystyle e\in E}$ um predicado. Cada condição de salto jump${\displaystyle (e)}$ é um predicado cujas variáveis livres são de ${\displaystyle X\cup X'}$.
• Um conjunto finito de eventos ${\displaystyle \Sigma }$, e uma função de rotulagem de arestas event: ${\displaystyle E\rightarrow \Sigma }$ 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

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. v d e