Hybridsystem

Ett hybridsystem är ett dynamiskt system som uppvisar både kontinuerligt och diskret dynamiskt beteende - ett system som både kan flyta (beskrivs av en differentialekvation ) och hoppa (beskrivs av en tillståndsmaskin eller automat ). Ofta används termen "hybrid dynamiskt system" för att särskilja hybridsystem som de som kombinerar neurala nät och fuzzy logik , eller elektriska och mekaniska drivlinor. Ett hybridsystem har fördelen av att omfatta en större klass av system inom sin struktur, vilket möjliggör mer flexibilitet vid modellering av dynamiska fenomen.

I allmänhet definieras tillståndet för ett hybridsystem av värdena för de kontinuerliga variablerna och ett diskret läge . Tillståndet ändras antingen kontinuerligt, enligt ett flödesförhållande , eller diskret enligt en kontrollgraf . Kontinuerligt flöde är tillåtet så länge så kallade invarianter håller, medan diskreta övergångar kan inträffa så snart givna hoppvillkor är uppfyllda. Diskreta övergångar kan vara associerade med händelser .

Exempel

Hybridsystem har använts för att modellera flera cyberfysiska system, inklusive fysiska system med effekt , logikdynamiska styrenheter och till och med överbelastning på Internet .

Studsboll

Ett kanoniskt exempel på ett hybridsystem är den studsande bollen , ett fysiskt system med slag. Här släpps bollen (tänkt som en punktmassa) från en initial höjd och studsar från marken och försvinner sin energi med varje studs. Bollen uppvisar kontinuerlig dynamik mellan varje studs; men när bollen träffar marken, genomgår dess hastighet en diskret förändring som modelleras efter en oelastisk kollision . En matematisk beskrivning av den studsande bollen följer. Låt $x_{1}$ vara kulans höjd och $x_{2}$ vara kulans hastighet. Ett hybridsystem som beskriver bollen är som följer:

När $x\in C=\{x_{1}>0\}$ styrs flödet av ${\displaystyle {\dot {x}}_{1}=x_{2},{\dot {x}}_{2}=-g} ,$ där $g$ är accelerationen på grund av gravitationen. Dessa ekvationer säger att när bollen är ovan mark dras den till marken av gravitationen.

När $x\in D=\{x_{1}=0\}$ styrs hopp av ${ \displaystyle x_{1}^{+}=x_{1},x_{2}^{+}=-\gamma x_{2}} , där$ < $\displaystyle 0<\gamma <1}$ är en spridningsfaktor. Detta säger att när kulans höjd är noll (den har påverkat marken), så vänds dess hastighet och minskas med faktorn $\gamma$ . Detta beskriver effektivt den oelastiska kollisionens natur.

Den studsande bollen är ett särskilt intressant hybridsystem, eftersom det uppvisar Zeno -beteende. Zenobeteende har en strikt matematisk definition, men kan informellt beskrivas som att systemet gör ett oändligt antal hopp på en begränsad tid. I det här exemplet tappar den energi varje gång bollen studsar, vilket gör att de efterföljande hoppen (slag mot marken) blir närmare och närmare varandra i tiden.

Det är anmärkningsvärt att den dynamiska modellen är komplett om och endast om man lägger till kontaktkraften mellan marken och bollen. Utan krafter kan man verkligen inte definiera den studsande bollen och modellen är, ur mekanisk synvinkel, meningslös. Den enklaste kontaktmodellen som representerar växelverkan mellan bollen och marken är komplementaritetsrelationen mellan kraften och avståndet (gapet) mellan bollen och marken. Detta skrivs som $0\leq \lambda \perp x_{1}\geq 0.$ En sådan kontaktmodell innehåller inte magnetiska krafter, inte heller limningseffekter. När komplementaritetsrelationerna är inne, kan man fortsätta att integrera systemet efter att stötarna har ackumulerats och försvunnit: systemets jämvikt är väldefinierat som den statiska jämvikten för bollen på marken, under inverkan av gravitationen kompenserad av kontaktkraft $\lambda$ . Man märker också från grundläggande konvex analys att komplementaritetsrelationen på motsvarande sätt kan skrivas om som inkluderingen i en normal kon, så att den studsande bolldynamiken är en differentiell inkludering i en normal kon till en konvex uppsättning. Se kapitel 1, 2 och 3 i Acary-Brogliatos bok som citeras nedan (Springer LNACM 35, 2008). Se även de andra referenserna om icke-slät mekanik.

Hybridsystemverifiering _

Det finns metoder för att automatiskt bevisa egenskaper hos hybridsystem (t.ex. några av verktygen som nämns nedan). Vanliga tekniker för att bevisa säkerheten för hybridsystem är beräkning av nåbara uppsättningar, abstraktionsförfining och barriärcertifikat .

De flesta verifieringsuppgifter är oavgjorda, vilket gör allmänna verifieringsalgoritmer omöjliga . Istället analyseras verktygen för deras kapacitet på benchmarkproblem. En möjlig teoretisk karaktärisering av detta är algoritmer som lyckas med hybridsystemverifiering i alla robusta fall, vilket innebär att många problem för hybridsystem, även om de är oavgjorda, är åtminstone nästan avgörbara.

Andra modelleringsmetoder

Två grundläggande hybridsystemmodelleringsmetoder kan klassificeras, en implicit och en explicit. Det explicita tillvägagångssättet representeras ofta av en hybridautomat , ett hybridprogram eller ett hybrid Petri-nät . Det implicita tillvägagångssättet representeras ofta av bevakade ekvationer för att resultera i system av differentialalgebraiska ekvationer (DAE) där de aktiva ekvationerna kan ändras, till exempel med hjälp av en hybridbindningsgraf .

Som en enhetlig simuleringsmetod för hybridsystemanalys finns det en metod baserad på DEVS- formalism där integratörer för differentialekvationer kvantiseras till atomära DEVS -modeller. Dessa metoder genererar spår av systembeteenden på ett diskret händelsesystemsätt som skiljer sig från diskreta tidssystem. Detaljerad information om detta tillvägagångssätt kan hittas i referenser [Kofman2004] [CF2006] [Nutaro2010] och mjukvaruverktyget PowerDEVS .

Verktyg

• Ariadne : Ett C++-bibliotek för (numeriskt rigorös) nåbarhetsanalys av olinjära hybridsystem
• C2E2 : Icke-linjär hybridsystemverifierare
• CORA Arkiverad 2018-07-31 på Wayback Machine : A MATLAB Toolbox för nåbarhetsanalys av cyberfysiska system, inklusive hybridsystem
• Flow* : Ett verktyg för nåbarhetsanalys av olinjära hybridsystem
• HyCreate : Ett verktyg för att överapproximera nåbarheten för hybridautomater
• HyEQ : En hybridsystemlösare för Matlab
• HyPro : Ett C++-bibliotek för tillståndsuppsättningsrepresentationer för hybridsystems nåbarhetsanalys
• HSolver : Verifiering av hybridsystem
• HyTech : En modellkontroll för hybridsystem
• JuliaReach : En verktygslåda för uppsättningsbaserad nåbarhet
• KeYmaera : En hybridsatsbevisare för hybridsystem
• PHAVer : Polyhedral Hybrid Automaton Verifier
• PowerDEVS : Ett generellt mjukvaruverktyg för DEVS-modellering och -simulering inriktat på simulering av hybridsystem
• SCOTS : Ett verktyg för syntes av konstruktionsstyrda kontroller för hybridsystem
• SpaceEx : State-Space Explorer
• S-TaLiRo : En MATLAB-verktygslåda för verifiering av hybridsystem med avseende på tidslogikspecifikationer

Se även

• Hybrid automat
• Glidlägeskontroll
• System med variabel struktur
• Variabel strukturkontroll
• Gemensam spektral radie
• Cyberfysiskt system
• Beteendeträd (artificiell intelligens, robotik och kontroll)
• Hoppprocess (i samband med sannolikhet ), ett exempel på ett (stokastiskt) hybridsystem med nollflödeskomponent
• Styckvis deterministisk Markov-process (PDMP), ett exempel på ett (stokastiskt) hybridsystem och en generalisering av hoppprocessen
• Jump diffusion , ett exempel på ett (stokastiskt) hybridsystem och en generalisering av PDMP

Vidare läsning

• Henzinger, Thomas A. (1996), "The Theory of Hybrid Automata", 11th Annual Symposium on Logic in Computer Science (LICS), IEEE Computer Society Press, s. 278–292, arkiverad från originalet 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 algorithmic analysis of hybrid systems" , Theoretical Computer Science , 138 (1): 3–34, doi : 10.1016/0304-3975(94)00202-T , hdl : 1813/6241 , från originalet 2010-01-27
•   Goebel, Rafal; Sanfelice, Ricardo G.; Teel, Andrew R. (2009), "Hybrid dynamical 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.170344/10.171634
• [CF2006]   Francois E. Cellier och Ernesto Kofman (2006), Continuous System Simulation (första upplagan), Springer, ISBN 978-0-387-26102-7
• [Nutaro2010] James Nutaro (2010), Byggprogramvara för simulering: teori, algoritmer och applikationer i C++ ( första upplagan), Wiley
•   Brogliato, Bernard; Tanwani, Aneel (2020), "Dynamiska system kopplade med monotona set-valued operators: Formalisms, Applications, well-posedness and stabilitet" ( PDF) , SIAM Review , 62 (1): 3–129, doi : 10.1137/18M1234795 , S2CID 212727046

externa länkar

• IEEE CSS Committee on Hybrid Systems Arkiverad 2021-06-26 på Wayback Machine