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:

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

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.