Sistema híbrido

Un sistema híbrido es un sistema dinámico que exhibe un comportamiento dinámico tanto continuo como discreto: un sistema que puede fluir (descrito mediante una ecuación diferencial) y salto (descrito por una máquina de estados o autómata). A menudo, el término "sistema dinámico híbrido" se utiliza para distinguir sistemas híbridos como aquellos que combinan redes neuronales y lógica difusa, o líneas motrices eléctricas y mecánicas. Un sistema híbrido tiene la ventaja de abarcar una clase más amplia de sistemas dentro de su estructura, lo que permite una mayor flexibilidad en el modelado de fenómenos dinámicos.

En general, el estado de un sistema híbrido se define por los valores de las variables continuas y un modo discreto. El estado cambia de forma continua, según una condición de flujo, o discretamente según un gráfico de control. Se permite el flujo continuo siempre que se mantengan las llamadas invariantes, mientras que pueden ocurrir transiciones discretas tan pronto como se cumplan las condiciones de salto dadas. Las transiciones discretas pueden estar asociadas con eventos.

Ejemplos

Los sistemas híbridos se han utilizado para modelar varios sistemas ciberfísicos, incluidos sistemas físicos con impacto, controladores lógico-dinámicos e incluso congestión de Internet.

Bola que rebota

Un ejemplo canónico de un sistema híbrido es la bola de rebote, un sistema físico con impacto. Aquí, la pelota (pensada como punto-masa) se deja caer de una altura inicial y rebota del suelo, disipando su energía con cada rebote. La bola exhibe dinámicas continuas entre cada onza; sin embargo, a medida que la bola impacta el suelo, su velocidad sufre un cambio discreto modelado después de una colisión inelástica. Una descripción matemática de la bola de rebote sigue. Vamos ${displaystyle x_{1}}$ ser la altura de la bola y ${displaystyle x_{2}$ Sé la velocidad de la bola. Un sistema híbrido que describe la bola es el siguiente:

Cuando ${displaystyle xin C={x_{1} {}}}} {f}} {f}} {f}}$, el flujo se rige por ${displaystyle {dot {}_{1}=x_{2},{dot {x}_{2}=-g}$, Donde ${displaystyle g}$ es la aceleración debido a la gravedad. Estas ecuaciones indican que cuando la bola está por encima del suelo, se está dibujando al suelo por gravedad.

Cuando ${displaystyle xin D={x_{1}=0}$, los saltos se rigen por ${displaystyle x_{1}{+}=x_{1},x_{2}{+}=-gamma x_{2}}$, Donde ${displaystyle 0.$ es un factor de disipación. Esto es decir que cuando la altura de la bola es cero (ha impactado el suelo), su velocidad se revierte y disminuye por un factor de ${displaystyle gamma }$. Efectivamente, esto describe la naturaleza de la colisión inelástica.

La pelota que rebota es un sistema híbrido especialmente interesante, ya que muestra el comportamiento de Zeno. El comportamiento de Zenón tiene una definición matemática estricta, pero puede describirse informalmente como el sistema que realiza un número infinito de saltos en una cantidad de tiempo finita. En este ejemplo, cada vez que la pelota rebota pierde energía, haciendo que los saltos posteriores (impactos con el suelo) se acerquen cada vez más en el tiempo.

Cabe destacar que el modelo dinámico está completo si se agrega la fuerza de contacto entre el suelo y la pelota. De hecho, sin fuerzas, no se puede definir adecuadamente la bola de rebote y el modelo es, desde un punto de vista mecánico, sin sentido. El modelo de contacto más simple que representa las interacciones entre la bola y el suelo, es la relación de complementariedad entre la fuerza y la distancia (la brecha) entre la bola y el suelo. Esto está escrito como ${displaystyle 0leq lambda perp x_{1}geq 0.}$Tal modelo de contacto no incorpora fuerzas magnéticas ni efectos de cola. Cuando las relaciones de complementariedad están en, se puede seguir integrando el sistema después de que los impactos se hayan acumulado y desaparecido: el equilibrio del sistema está bien definido como el equilibrio estático de la bola en el suelo, bajo la acción de gravedad compensada por la fuerza de contacto ${displaystyle lambda }$. También se observa desde el análisis convexo básico que la relación de complementariedad puede ser reescrita como la inclusión en un cono normal, de modo que la dinámica de bolas rebotando es una inclusión diferencial en un cono normal a un conjunto convexo. See Chapters 1, 2 and 3 in Acary-Brogliato's book cited below (Springer LNACM 35, 2008). Vea también las otras referencias sobre mecánicas no mohoth.

Verificación de sistemas híbridos

Existen enfoques para probar automáticamente las propiedades de los sistemas híbridos (por ejemplo, algunas de las herramientas que se mencionan a continuación). Las técnicas comunes para demostrar la seguridad de los sistemas híbridos son el cálculo de conjuntos alcanzables, el refinamiento de la abstracción y los certificados de barrera.

La mayoría de las tareas de verificación son indecidibles, lo que hace imposibles los algoritmos de verificación generales. En cambio, las herramientas se analizan por sus capacidades en problemas de referencia. Una posible caracterización teórica de esto son los algoritmos que tienen éxito con la verificación de sistemas híbridos en todos los casos robustos, lo que implica que muchos problemas de los sistemas híbridos, si bien son indecidibles, son al menos cuasi-decidibles.

Otros enfoques de modelado

Se pueden clasificar dos enfoques básicos de modelado de sistemas híbridos, uno implícito y otro explícito. El enfoque explícito suele estar representado por un autómata híbrido, un programa híbrido o una red de Petri híbrida. El enfoque implícito a menudo se representa mediante ecuaciones guardadas para dar como resultado sistemas de ecuaciones algebraicas diferenciales (DAE) donde las ecuaciones activas pueden cambiar, por ejemplo mediante un gráfico de enlaces híbridos.

Como enfoque de simulación unificada para el análisis de sistemas híbridos, existe un método basado en el formalismo DEVS en el que los integradores de ecuaciones diferenciales se cuantifican en modelos DEVS atómicos. Estos métodos generan rastros de comportamientos del sistema en forma de sistema de eventos discretos que son diferentes de los sistemas de tiempo discreto. Se pueden encontrar detalles de este enfoque en las referencias [Kofman2004] [CF2006] [Nutaro2010] y la herramienta de software PowerDEVS.

Herramientas de software

Simulación

• HyEQ Toolbox: Resolver sistema híbrido para MATLAB y Simulink
• PowerDEVS: Herramienta de uso general para el modelado y simulación DEVS (Discrete Event System) orientada a la simulación de sistemas híbridos

Alcancebilidad

• Ariadne: Biblioteca C+ para el análisis de capacidad de alcance (numericalmente riguroso) de sistemas híbridos no lineales
• CORA: Una caja de herramientas MATLAB para el análisis de la capacidad de los sistemas ciberfísicos, incluidos los sistemas híbridos
• Flujo*: Una herramienta para el análisis de la accesibilidad de sistemas híbridos no lineales
• HyCreate: Una herramienta para alcanzar la automata híbrida
• HyPro: biblioteca C+ para las representaciones establecidas por el estado para el análisis de capacidad de los sistemas híbridos
• JuliaReach: Una caja de herramientas para la accesibilidad basada en conjunto

Lógica temporal y otras verificaciones

• C2E2: verificador de sistema híbrido no lineal
• HyTech: Controlador modelo para sistemas híbridos
• HSolver: Herramienta de verificación para sistemas híbridos
• KeYmaera: Theorem prover para sistemas híbridos
• PHAVer: verificador autómata híbrido poliedral
• S-TaLiRo: MATLAB caja de herramientas para la verificación de sistemas híbridos con respecto a las especificaciones lógicas temporales

Otro

• SCOTS: Herramienta para la síntesis de controladores correctos por construcción para sistemas híbridos
• SpaceEx: State-space explorer