Bernstein-based polynomial approach to study the stability of switched systems and formal verification using HOL Light

तकनीकी सारांश: स्विच किए गए सिस्टम की स्थिरता और औपचारिक सत्यापन के लिए बर्नस्टीन-आधारित बहुपद दृष्टिकोण

समस्या विवरण
स्विच किए गए सिस्टम (Switched systems), जो एक स्विचिंग सिग्नल द्वारा नियंत्रित कई उप-प्रणालियों (subsystems) से बने होते हैं, स्थिरता विश्लेषण में महत्वपूर्ण चुनौतियाँ प्रस्तुत करते हैं। पारंपरिक विधियाँ अक्सर सिस्टम के पूर्ण व्यवहार का एक एकीकृत गणितीय विवरण प्रदान करने में संघर्ष करती हैं, विशेष रूप से जब स्विचिंग सिग्नल जटिल हो (जैसे कि अवस्था-निर्भर या समय-निर्भर)। हालांकि इन प्रणालियों के विश्लेषण के लिए कई विधियाँ मौजूद हैं, लेकिन एक ऐसे फॉर्मूलेशन की आवश्यकता है जो स्विचिंग तर्क (switching logic) को एक निरंतर बहुपद अभिव्यक्ति (continuous polynomial expression) में परिवर्तित कर सके, जिससे ल्यापुनोव फलनों (Lyapunov functions) का निर्माण सुगम हो सके और कठोर औपचारिक सत्यापन (formal verification) सक्षम हो सके।

कार्यप्रणाली
यह शोध पत्र बर्नस्टीन इंटरपोलेशन (Bernstein interpolation) का उपयोग करके स्विच किए गए सिस्टम को पुनर्गठित करने की एक रणनीति प्रस्तावित करता है। मुख्य दृष्टिकोण में निम्नलिखित चरण शामिल हैं:

1. बहुपद पुनर्गठन (Polynomial Reformulation): स्विचिंग सिग्नल $\sigma$, जो उप-प्रणालियों $f_i$ की सक्रियता को निर्देशित करता है, को बर्नस्टीन बहुपदों का उपयोग करके अनुमानित किया जाता है। स्विचिंग सिग्नल को बर्नस्टीन आधार फलनों (Bernstein basis functions) के एक रैखिक संयोजन के रूप में व्यक्त करके, संपूर्ण स्विच किया गया सिस्टम (जो मूल रूप से खंडित अवकल समीकरणों [piecewise differential equations] द्वारा परिभाषित है) एक एकल, एकीकृत बहुपद अभिव्यक्ति में बदल जाता है।

   • सिस्टम को उप-प्रणालियों के एक उत्तल संयोजन (convex combination) के रूप में वर्णित किया जाता है: $\dot{x} = \sum f_i(x)\sigma_i$, जहाँ $\sum \sigma_i = 1$ और $\sigma_i \geq 0$ है।
   • स्विचिंग सिग्नल $\sigma_i$ को इसके बर्नस्टीन श्रृंखला सन्निकटन (Bernstein series approximation) $B_{i,m}^\sigma(\sigma(\nu), \nu)$ द्वारा प्रतिस्थापित किया जाता है, जिसके परिणामस्वरूप एक एकल बहुपद अवकल समीकरण द्वारा वर्णित "B-स्विच्ड सिस्टम" प्राप्त होता है।

2. स्विचिंग प्रकारों को संभालना: यह विधि विभिन्न स्विचिंग व्यवहारों को समायोजित करती है:

   • अवस्था-निर्भर स्विचिंग (State-dependent switching): इसे साइन फंक्शन (जैसे, $\sigma \equiv \text{sign}(\delta x_1 x_2)$) का उपयोग करके मॉडल किया जाता है, जिसे एक विशिष्ट डिग्री $m$ के बर्नस्टीन बहुपदों द्वारा अनुमानित किया जाता है।
   • समय-निर्भर स्विचिंग (Time-dependent switching): आवधिक सक्रियण (periodic activation) को दर्शाने के लिए पल्स फंक्शन का उपयोग किया जाता है।
   • लचीलापन: बर्नस्टीन बहुपद की डिग्री $m$ को सन्निकटन को परिष्कृत करने के लिए समायोजित किया जा सकता है, या उच्च परिशुद्धता के लिए संयोजन नियमों (composition rules) को लागू किया जा सकता है, हालांकि इससे परिणामी अभिव्यक्तियों की जटिलता बढ़ जाती है।

3. औपचारिक सत्यापन (Formal Verification): एक बार जब सिस्टम को एक बहुपद के रूप में प्रस्तुत कर दिया जाता है, तो लेखक स्थिरता गुणों को औपचारिक रूप से सत्यापित करने के लिए HOL Light प्रूफ असिस्टेंट का उपयोग करने का प्रस्ताव करते हैं।

   • एक उम्मीदवार ल्यापुनोव फलन $V(x)$ को बहुपद सिस्टम के लिए पहचाना जाता है।
   • सत्यापन कार्य को एक परिभाषित डोमेन $D$ पर असमिका $\dot{V}(x) < \epsilon$ (जहाँ $\epsilon$ एक छोटा धनात्मक स्थिरांक है) को सिद्ध करने में कम किया जाता है।
   • यह टेलर सन्निकटन के साथ अंतराल अंकगणित (interval arithmetic with Taylor approximations) का उपयोग करके प्राप्त किया जाता है, जो एक ऐसी विधि है जिसे पहले फ्लाईस्पेक (Flyspeck) प्रोजेक्ट में मान्य किया गया था। यह प्रमाणित करता है कि निर्दिष्ट सीमाओं के भीतर ल्यापुनोव व्युत्पन्न (Lyapunov derivative) ऋणात्मक (या शून्य के पर्याप्त करीब) है।

मुख्य परिणाम
शोध पत्र मौजूदा साहित्य से प्राप्त दो संख्यात्मक उदाहरणों के माध्यम से प्रस्तावित दृष्टिकोण का प्रदर्शन करता है, जो "मानक" स्विच किए गए सिस्टम के विरुद्ध "B-स्विच्ड" बहुपद प्रतिनिधित्व की तुलना करता है:

• उदाहरण 1 (स्थिर सिस्टम): दो स्थिर उप-प्रणालियों वाले एक रैखिक स्विच किए गए सिस्टम का विश्लेषण किया गया। बर्नस्टीन सन्निकटन ने मानक सिस्टम के स्थिर व्यवहार की सफलतापूर्वक नकल की।
• उदाहरण 2 (अस्थिर सिस्टम): अस्थिर उप-प्रणालियों वाले एक रैखिक स्विच किए गए सिस्टम का विश्लेषण किया गया। विधि ने विचलन व्यवहार को सही ढंग से पकड़ा, यह नोट करते हुए कि जैसे-जैसे अवस्था उत्पाद $x_1 x_2$ अंतराल $[0, 1]$ से आगे बढ़ता है, बर्नस्टीन श्रृंखला स्वाभाविक रूप से विचलित होती है, जो सिस्टम की अस्थिरता को दर्शाती है।
• औपचारिक सत्यापन: एक बुनियादी रैखिक स्थिर सिस्टम का उपयोग HOL Light सत्यापन प्रक्रिया को प्रदर्शित करने के लिए किया गया। लेखकों ने एक औपचारिक प्रमाण प्रमाण पत्र (formal proof certificate) सफलतापूर्वक उत्पन्न किया, जो पुष्टि करता है कि अंतराल $[0, 1]$ के भीतर एक द्विघाती ल्यापुनोव फलन का व्युत्पन्न एक दहलीज ($\epsilon = 0.01$) से नीचे रहता है।

महत्व और दावे
लेखक इस कार्य को एक प्रारंभिक अध्ययन के रूप में प्रस्तुत करते हैं जिसमें विशिष्ट योगदान और सीमाएँ हैं:

• एकीकरण (Unification): प्राथमिक योगदान बर्नस्टीन इंटरपोलेशन के माध्यम से कई स्विचिंग उप-प्रणालियों को एक एकल बहुपद अभिव्यक्ति में "एकीकृत" करने की क्षमता है। यह ल्यापुनोव उम्मीदवार फलनों की खोज को सरल बनाता है।
• औपचारिक प्रमाणन (Formal Certification): यह दृष्टिकोण संख्यात्मक सिमुलेशन और औपचारिक प्रमाण के बीच के अंतर को पाटता है, जिससे HOL Light असिस्टेंट को प्राप्त ल्यापुनोव फलनों के स्थिरता गुणों को सत्यापित करने की अनुमति मिलती है।
• सीमित दायरा: शोध पत्र स्पष्ट रूप से बताता है कि यह मान लेता है कि B-स्विच्ड सिस्टम के स्थिरता गुण मानक स्विच किए गए सिस्टम के समान हैं (कम से कम ल्यापुनोव स्थिरता के संबंध में), लेकिन यह अभी तक इस समानता को कठोरता से सिद्ध करने का दावा नहीं करता है।
• भावी कार्य: लेखक भविष्य के अनुसंधान के लिए कई क्षेत्रों की पहचान करते हैं, जिनमें शामिल हैं:
  • मानक और B-स्विच्ड निरूपणों के बीच स्थिरता के संबंध में पूर्ण गणितीय समानता को सिद्ध करना।
  • गैर-रैखिक और गैर-बहुपद प्रणालियों तक विधि का विस्तार करना।
  • पहचाने गए उम्मीदवारों को केवल सत्यापित करने के बजाय "इष्टतम" ल्यापुनोव फलनों की गणना करने के लिए सम-ऑफ-स्क्वेयर्स (Sum-of-Squares - SOS) उपकरणों का उपयोग करना।

निष्कर्षतः, यह शोध पत्र एक नवीन ढांचे का प्रस्ताव करता है जो स्विच किए गए सिस्टम के विश्लेषण को एक बहुपद समस्या में बदलने के लिए बर्नस्टीन बहुपदों का लाभ उठाता है, जिसे औपचारिक सत्यापन उपकरणों के माध्यम से हल किया जा सकता है, जो कठोर स्थिरता प्रमाणन के लिए एक संभावित मार्ग प्रदान करता है।