Hibrit sistem

Bir hibrit sistem, hem sürekli hem de ayrık dinamik davranış sergileyen dinamik bir sistemdir. Başka bir değişle hem akabilen (bir diferansiyel denklemle tanımlanır) hem de zıplayabilen (bir durum makinesi veya otomat tarafından tanımlanır) bir sistemtir. Genellikle, "hibrit dinamik sistem" terimi, sinir ağlarını ve bulanık mantığı veya elektrikli ve mekanik aktarma organlarını birleştirenler gibi hibrit sistemleri ayırt etmek için kullanılmaktadır. Bir hibrit sistem, yapısı içinde daha geniş bir sistem sınıfını kapsama avantajına sahiptir. Ayrıca dinamik olduların modellenmesinde daha fazla esneklik sağlamaktadır.

Genel olarak, bir hibrit sistemin durumu, sürekli değişkenlerin değerleri ve ayrık bir mod ile tanımlanmaktadır. Durum, bir akış koşuluna göre sürekli olarak veya bir kontrol grafiğine göre ayrık olarak değişmektedir. Sözde değişmezler tutulduğu sürece sürekli akışa izin verilirken, verilen atlama koşulları karşılanır karşılanmaz ayrık geçişler meydana gelmektedir. Ayrık geçişler olaylarla ilişkilendirilebilmektedir.

Örnekler

Hibrit sistemler, darbeli fiziksel sistemler, mantıksal-dinamik kontrolörler ve hatta internet tıkanıklığı dahil olmak üzere çeşitli siber-fiziksel sistemleri modellemek için kullanılmaktadır

Zıplayan top

Melez sistemin kanonik bir örneği, çarpma etkisi olan fiziksel bir sistem olan zıplayan toptur. Burada, top (bir nokta kütlesi olarak düşünülmektedir) ilk yükseklikten düşürülmektedir. Ardından yerden sıçramaktadır. Her sıçramada enerjisini yaymaktadır. Top, her sekme arasında sürekli dinamikler sergilemektedir. Bununla birlikte, top yere çarptığında, hızı esnek olmayan bir çarpışmadan sonra modellenen ayrı bir değişime uğramaktadır. Zıplayan topun matematiksel bir açıklaması aşağıdaki şekildedir. Topun yüksekliği $x_{1}$ , topun hızı $x_{2}$ olarak belirlensin, topu tanımlayan bir hibrit sistem aşağıdaki gibidir:

$x\in C=\{x_{1}>0\}$ olduğunda, akış tarafından yönetilir. ${\dot {x}}_{1}=x_{2},{\dot {x}}_{2}=-g$ , burada g yerçekimi ivmesidir. Bu denklemler, topun yerden yüksekteyken yerçekimi ile yere çekildiğini belirtmektedir.

$x\in D=\{x_{1}=0\}$ olduğunda, atlamalar tarafından yönetilir $x_{1}^{+}=x_{1},x_{2}^{+}=-\gamma x_{2}$ , burada $0<\gamma <1$ aralığında bir dağılma faktörüdür. Bu, topun yüksekliği sıfır olduğunda (yere çarptığında), hızının tersine döndüğü ve bir kat azaldığı anlamına gelmektedir. Etkili bir şekilde, bu esnek olmayan çarpışmanın doğasını açıklamaktadır.

Zıplayan top, Zeno davranışı sergilediği için özellikle ilginç bir melez sistemdir. Zeno davranışının katı bir matematiksel tanımı vardır. Ancak gayri resmi olarak sonlu bir zaman diliminde sonsuz sayıda sıçrama yapan sistem olarak tanımlanabilmektedir. Bu örnekte, top her zıpladığında enerji kaybetmekte ve sonraki sıçramaları (yerle olan darbeleri) zamanla birbirine daha da yakınlaştırmaktadır.

Dinamik modelin ancak ve ancak zemin ve top arasındaki temas kuvveti eklendiğinde tamamlanmış olması dikkate değerdir. Gerçekten de kuvvetler olmadan zıplayan top tam olarak tanımlanamaz ve model mekanik bir bakış açısından anlamsızdır. Top ve yer arasındaki etkileşimleri temsil eden en basit temas modeli, kuvvet ile top ile yer arasındaki mesafe (boşluk) arasındaki tamamlayıcılık ilişkisidir. Bu şekilde de yazılmaktadır $0\leq \lambda \perp x_{1}\geq 0.$ Böyle bir temas modeli, manyetik kuvvetleri veya yapıştırma etkilerini içermemektedir. Tamamlayıcılık ilişkileri içindeyken, etkiler birikip ortadan kalktıktan sonra sistemi bütünleştirmeye devam edebilmektedir. Sistemin dengesi, topun yerçekimi etkisi altında yerdeki statik dengesi olarak temas kuvveti $\lambda$ ile daha iyi tanımlanmaktadır. Temel dışbükey analizden de fark edilir ki, tamamlayıcılık ilişkisi, normal bir koniye dahil etme olarak eşdeğer olarak yeniden yazılmaktadır. Böylece zıplayan top dinamiği, normal bir koniden bir dışbükey kümeye diferansiyel bir dahil etmedir

Hibrit Sistem Doğrulaması

Hibrit sistemlerin özelliklerini otomatik olarak kanıtlamaya yönelik yaklaşımlar vardır. Hibrit sistemlerin güvenliğini kanıtlamak için yaygın teknikler, erişilebilir kümelerin hesaplanması, soyutlama iyileştirme ve bariyer sertifikalarıdır.

Çoğu doğrulama görevi karar verilemez,^[1] bu da genel doğrulama algoritmalarını imkansız hale getirmektedir. Bunun yerine araçlar, kıyaslama problemlerindeki yetenekleri açısından analiz edilmektedir. Bunun olası bir teorik karakterizasyonu, tüm sağlam durumlarda hibrit sistem doğrulaması ile başarılı olan algoritmalardır.^[2] Bu, hibrit sistemler için birçok problemin karar verilemese de en azından yarı karar verilebilir olduğunu ima etmektedir.^[3]

Diğer modelleme yaklaşımları

İki temel hibrit sistem modelleme yaklaşımı, örtük ve açık bir şekilde sınıflandırılmaktadır. Açık yaklaşım genellikle hibrit bir otomat, bir hibrit program veya bir hibrit Petri ağı ile temsil edilmektedir. Örtük yaklaşım genellikle, örneğin bir hibrit bağ grafiği aracılığıyla aktif denklemlerin değişebileceği diferansiyel cebirsel denklem sistemleri (DAE'ler) ile sonuçlanmak üzere korumalı denklemlerle temsil edilmektedir.

Hibrit sistem analizi için birleşik bir simülasyon yaklaşımı olarak, diferansiyel denklemler için entegratörlerin atomik DEVS modellerine nicelleştirildiği DEVS formalizmine dayalı bir yöntem vardır. Bu yöntemler, ayrık zamanlı sistemlerden farklı olarak ayrık olay sistemi tarzında sistem davranışlarının izlerini üretmektedir.

Araçlar

Ariadne 24 Şubat 2021 tarihinde Wayback Machine sitesinde arşivlendi.: Doğrusal olmayan hibrit sistemlerin (sayısal olarak titiz) erişilebilirlik analizi için bir C++ kitaplığı
C2E2 26 Haziran 2021 tarihinde Wayback Machine sitesinde arşivlendi.: Doğrusal olmayan hibrit sistem doğrulayıcı
CORA 31 Temmuz 2018 tarihinde Wayback Machine sitesinde arşivlendi.: Hibrit sistemler de dahil olmak üzere siber-fiziksel sistemlerin erişilebilirlik analizi için bir MATLAB Araç Kutusu
Flow* 30 Haziran 2021 tarihinde Wayback Machine sitesinde arşivlendi.: Doğrusal olmayan hibrit sistemlerin erişilebilirlik analizi için bir araç
HyCreate 21 Mart 2021 tarihinde Wayback Machine sitesinde arşivlendi.: Hibrit Otomatların Erişilebilirliğini Fazla Tahmin Etmek İçin Bir Araç
HyEQ 30 Haziran 2021 tarihinde Wayback Machine sitesinde arşivlendi.: Matlab için Hibrit Sistem Çözücü
HyPro 26 Haziran 2021 tarihinde Wayback Machine sitesinde arşivlendi.: Hibrit sistemlerin erişilebilirlik analizi için durum seti temsilleri için bir C kütüphanesi
HSolver 18 Şubat 2021 tarihinde Wayback Machine sitesinde arşivlendi.: Hibrit Sistemlerin Doğrulanması
HyTech 10 Haziran 2017 tarihinde Wayback Machine sitesinde arşivlendi.: Hibrit Sistemler İçin Bir Model Denetleyicisi
JuliaReach^{[ölü/kırık bağlantı]}: Küme Tabanlı Erişilebilirlik için Bir Araç Kutusu
KeYmaera 26 Haziran 2021 tarihinde Wayback Machine sitesinde arşivlendi.: Hibrit Sistemler İçin Bir Hibrit Teorem Kanıtı
PHAVer 26 Haziran 2021 tarihinde Wayback Machine sitesinde arşivlendi.: Çokyüzlü Hibrit Otomat Doğrulayıcı
PowerDEVS: Hibrit sistemlerin simülasyonuna yönelik DEVS modellemesi ve simülasyonu için genel amaçlı bir yazılım aracı
SCOTS 28 Haziran 2021 tarihinde Wayback Machine sitesinde arşivlendi.: Hibrit sistemler için yapıya göre doğru kontrolörlerin sentezi için bir araç
SpaceEx 28 Nisan 2021 tarihinde Wayback Machine sitesinde arşivlendi.: Durum-Uzay Gezgini
S-TaLiRo 14 Nisan 2021 tarihinde Wayback Machine sitesinde arşivlendi.: Temporal Logic Spesifikasyonlarına göre Hibrit Sistemlerin doğrulanması için bir MATLAB Araç Kutusu

Ayrıca bakılabilir

Daha fazla makale

Henzinger, Thomas A. (1996), "The Theory of Hybrid Automata", 11th Annual Symposium on Logic in Computer Science (LICS), IEEE Computer Society Press, ss. 278-292, 27 Ocak 2010 tarihinde kaynağından arşivlendi
The algorithmic analysis of hybrid systems, 27 Ocak 2010 tarihinde kaynağından arşivlendi, erişim tarihi: 26 Haziran 2021
Goebel, Rafal; Sanfelice, Ricardo G.; Teel, Andrew R. (2009), "Hybrid dynamical systems", IEEE Control Systems Magazine, 29 (2), ss. 28-93, doi:10.1109/MCS.2008.931718
Acary, Vincent; Brogliato, Bernard (2008), "Numerical Methods for Nonsmooth Dynamical Systems", Lecture Notes in Applied and Computational Mechanics, cilt 35
[Kofman2004] Kofman, E (2004), "Discrete Event Simulation of Hybrid Systems", SIAM Journal on Scientific Computing, 25 (5), ss. 1771-1797, CiteSeerX 10.1.1.72.2475 $2, doi:10.1137/S1064827502418379
[CF2006] Francois E. Cellier and Ernesto Kofman (2006), Continuous System Simulation, first, Springer, ISBN 978-0-387-26102-7
[Nutaro2010] James Nutaro (2010), Building Software for Simulation: Theory, Algorithms, and Applications in C++, first, Wiley
Brogliato, Bernard; Tanwani, Aneel (2020), "Dynamical systems coupled with monotone set-valued operators: Formalisms, Applications, well-posedness, and stability" (PDF), SIAM Review, 62 (1), ss. 3-129, doi:10.1137/18M1234795, 26 Haziran 2021 tarihinde kaynağından arşivlendi (PDF), erişim tarihi: 26 Haziran 2021

Ek bağlantı

IEEE CSS Committee on Hybrid Systems 26 Haziran 2021 tarihinde Wayback Machine sitesinde arşivlendi.

Kaynakça

^ Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya: What's Decidable about Hybrid Automata, Journal of Computer and System Sciences, 1998
^ Martin Fränzle: Analysis of Hybrid Systems: An ounce of realism can save an infinity of states, Springer LNCS 1683
^ Stefan Ratschan: Safety verification of non-linear hybrid systems is quasi-decidable, Formal Methods in System Design, volume 44, pp. 71-90, 2014, DOI:10.1007/s10703-013-0196-2

[1] Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya: What's Decidable about Hybrid Automata, Journal of Computer and System Sciences, 1998

[2] Martin Fränzle: Analysis of Hybrid Systems: An ounce of realism can save an infinity of states, Springer LNCS 1683

[3] Stefan Ratschan: Safety verification of non-linear hybrid systems is quasi-decidable, Formal Methods in System Design, volume 44, pp. 71-90, 2014, DOI:10.1007/s10703-013-0196-2

[1]

[2]

[3]