Sistema híbrido - Hybrid system

Um sistema híbrido é um sistema dinâmico que exibe comportamento dinâmico contínuo e discreto - um sistema que pode fluir (descrito por uma equação diferencial ) e saltar (descrito por uma máquina de estado ou autômato ). Freqüentemente, o termo "sistema dinâmico híbrido" é usado para distinguir sistemas híbridos, como aqueles que combinam redes neurais e lógica difusa , ou linhas de transmissão elétricas e mecânicas. Um sistema híbrido tem a vantagem de abranger uma classe maior de sistemas em sua estrutura, permitindo mais flexibilidade na modelagem de fenômenos dinâmicos.

Em geral, o estado de um sistema híbrido é definido pelos valores das variáveis ​​contínuas e um modo discreto . O estado muda continuamente, de acordo com uma condição de fluxo , ou discretamente, de acordo com um gráfico de controle . O fluxo contínuo é permitido enquanto os chamados invariantes se mantiverem, enquanto as transições discretas podem ocorrer assim que determinadas condições de salto forem satisfeitas. Transições discretas podem estar associadas a eventos .

Exemplos

Os sistemas híbridos têm sido usados ​​para modelar vários sistemas ciberfísicos, incluindo sistemas físicos com impacto , controladores lógico-dinâmicos e até mesmo congestionamento da Internet .

Bola quicando

Um exemplo canônico de sistema híbrido é a bola quicando , um sistema físico com impacto. Aqui, a bola (pensada como um ponto-massa) é lançada de uma altura inicial e quica no chão, dissipando sua energia a cada salto. A bola exibe uma dinâmica contínua entre cada salto; no entanto, conforme a bola atinge o solo, sua velocidade sofre uma mudança discreta modelada após uma colisão inelástica . Segue-se uma descrição matemática da bola quicando. Let ser a altura da bola e ser a velocidade da bola. Um sistema híbrido que descreve a bola é o seguinte:

Quando , o fluxo é governado por , onde está a aceleração da gravidade. Essas equações afirmam que, quando a bola está acima do solo, ela é atraída ao solo pela gravidade.

Quando , os saltos são governados por , onde está um fator de dissipação. Isso quer dizer que quando a altura da bola é zero (ela atingiu o solo), sua velocidade é revertida e diminuída por um fator de . Efetivamente, isso descreve a natureza da colisão inelástica.

A bola quicando é um sistema híbrido especialmente interessante, pois exibe o comportamento de Zeno . O comportamento de Zeno tem uma definição matemática estrita, mas pode ser descrito informalmente como o sistema que faz um número infinito de saltos em uma quantidade finita de tempo. Neste exemplo, cada vez que a bola quica, ela perde energia, fazendo com que os saltos subsequentes (impactos com o solo) se aproximem cada vez mais no tempo.

Vale ressaltar que o modelo dinâmico está completo se e somente se adicionarmos a força de contato entre o solo e a bola. Na verdade, sem forças, não se pode definir adequadamente a bola quicando e o modelo é, do ponto de vista mecânico, sem sentido. O modelo de contato mais simples que representa as interações entre a bola e o solo, é a relação de complementaridade entre a força e a distância (a lacuna) entre a bola e o solo. Isso está escrito como Esse modelo de contato não incorpora forças magnéticas nem efeitos de colagem. Estando as relações de complementaridade, pode-se continuar a integrar o sistema após os impactos terem se acumulado e desaparecido: o equilíbrio do sistema é bem definido como o equilíbrio estático da bola no solo, sob a ação da gravidade compensada pela força de contato . Também se nota da análise convexa básica que a relação de complementaridade pode ser reescrita equivalentemente como a inclusão em um cone normal, de modo que a dinâmica da bola quicando é uma inclusão diferencial em um cone normal em um conjunto convexo. Veja os capítulos 1, 2 e 3 no livro de Acary-Brogliato citado abaixo (Springer LNACM 35, 2008). Veja também as outras referências sobre mecânica não suave.

Verificação de sistemas híbridos

Existem abordagens para provar automaticamente as propriedades de sistemas híbridos (por exemplo, algumas das ferramentas mencionadas abaixo). As técnicas comuns para provar a segurança de sistemas híbridos são computação de conjuntos alcançáveis, refinamento de abstração e certificados de barreira .

A maioria das tarefas de verificação são indecidíveis, tornando impossíveis os algoritmos gerais de verificação. Em vez disso, as ferramentas são analisadas por seus recursos em problemas de benchmark. Uma possível caracterização teórica disso são os algoritmos que têm sucesso com a verificação de sistemas híbridos em todos os casos robustos, o que implica que muitos problemas para sistemas híbridos, embora indecidíveis, são pelo menos quase decidíveis.

Outras abordagens de modelagem

Duas abordagens básicas de modelagem de sistema híbrido podem ser classificadas, uma implícita e outra explícita. A abordagem explícita é freqüentemente representada por um autômato híbrido , um programa híbrido ou uma rede de Petri híbrida . A abordagem implícita é frequentemente representada por equações protegidas para resultar em sistemas de equações algébricas diferenciais (DAEs) onde as equações ativas podem mudar, por exemplo, por meio de um gráfico de ligação híbrida .

Como uma abordagem de simulação unificada para análise de sistema híbrido, existe um método baseado no formalismo DEVS no qual integradores para equações diferenciais são quantizados em modelos DEVS atômicos . Esses métodos geram traços de comportamentos do sistema na maneira do sistema de eventos discretos que são diferentes dos sistemas de tempo discretos. Detalhes dessa abordagem podem ser encontrados nas referências [Kofman2004] [CF2006] [Nutaro2010] e na ferramenta de software PowerDEVS .

Ferramentas

  • Ariadne : Uma biblioteca C ++ para análise de acessibilidade (numericamente rigorosa) de sistemas híbridos não lineares
  • C2E2 : verificador de sistema híbrido não linear
  • CORA : uma caixa de ferramentas MATLAB para análise de acessibilidade de sistemas ciberfísicos, incluindo sistemas híbridos
  • Fluxo * : Uma ferramenta para análise de acessibilidade de sistemas híbridos não lineares
  • HyCreate : uma ferramenta para superavaliação da acessibilidade de autômatos híbridos
  • HyEQ : um solucionador de sistema híbrido para Matlab
  • HyPro : uma biblioteca C ++ para representações de conjuntos de estados para análise de acessibilidade de sistemas híbridos
  • HSolver : Verificação de Sistemas Híbridos
  • HyTech : um verificador de modelo para sistemas híbridos
  • JuliaReach : uma caixa de ferramentas para acessibilidade baseada em conjuntos
  • KeYmaera : um provador de teorema híbrido para sistemas híbridos
  • PHAVer : Verificador de autômato híbrido poliédrico
  • PowerDEVS : Uma ferramenta de software de uso geral para modelagem e simulação DEVS orientada para a simulação de sistemas híbridos
  • SCOTS : Uma ferramenta para a síntese de controladores corretos por construção para sistemas híbridos
  • SpaceEx : State-Space Explorer
  • S-TaLiRo : Uma caixa de ferramentas MATLAB para verificação de sistemas híbridos com relação às especificações lógicas temporais

Veja também

Leitura adicional

  • Henzinger, Thomas A. (1996), "The Theory of Hybrid Automata", 11th Annual Symposium on Logic in Computer Science (LICS) , IEEE Computer Society Press, pp. 278-292, arquivado do original em 2010-01-27
  • Alur, Rajeev; Courcoubetis, Costas; Halbwachs, Nicolas; Henzinger, Thomas A .; Ho, Pei-Hsin; Nicollin, Xavier; Olivero, Alfredo; Sifakis, Joseph; Yovine, Sergio (1995), "The algoritmic analysis of hybrid systems" , Theoretical Computer Science , 138 (1): 3-34, doi : 10.1016 / 0304-3975 (94) 00202-T , hdl : 1813/6241 , arquivado do original em 27/01/2010
  • Goebel, Rafal; Sanfelice, Ricardo G .; Teel, Andrew R. (2009), "Hybrid dynamic systems", IEEE Control Systems Magazine , 29 (2): 28-93, doi : 10.1109 / MCS.2008.931718 , S2CID   46488751
  • Acary, Vincent; Brogliato, Bernard (2008), "Numerical Methods for Nonsmooth Dynamical Systems", Lecture Notes in Applied and Computational Mechanics , 35
  • [Kofman2004] Kofman, E (2004), "Discrete Event Simulation of Hybrid Systems", SIAM Journal on Scientific Computing , 25 (5): 1771–1797, CiteSeerX   10.1.1.72.2475 , doi : 10.1137 / S1064827502418379
  • [CF2006] Francois E. Cellier e Ernesto Kofman (2006), Continuous System Simulation (primeira edição), Springer, ISBN   978-0-387-26102-7
  • [Nutaro2010] James Nutaro (2010), Building Software for Simulation: Theory, Algorithms, and Applications in C ++ (primeira ed.), Wiley
  • Brogliato, Bernard; Tanwani, Aneel (2020), "Dynamical systems coupled with monotone set-value operator: Formalisms, Applications, well-posedness, and estabilidade" (PDF) , SIAM Review , 62 (1): 3-129, doi : 10.1137 / 18M1234795

links externos

Referências