Semi-Competitive Differential Game Logic

तकनीकी सारांश: अर्ध-प्रतिस्पर्धी विभेदक गेम लॉजिक (dGLsc)

समस्या विवरण
साइबर-फिजिकल सिस्टम्स (CPS) की सुरक्षा सत्यापन, विशेष रूप से वे जिनमें कई एजेंटों (जैसे, स्वायत्त वाहन, विमान) के बीच परस्पर क्रिया शामिल है, महत्वपूर्ण चुनौतियाँ प्रस्तुत करता है। पारंपरिक दृष्टिकोण अक्सर इन परस्पर क्रियाओं को 'डिफरेंशियल गेम लॉजिक' (dGL) का उपयोग करके मॉडल करते हैं, जो एक शून्य-योग (zero-sum), प्रतिकूल संबंध मानता है जहाँ एक खिलाड़ी का लाभ दूसरे की हानि होता है। हालाँकि यह सुरक्षित परिणाम देता है, लेकिन यह अक्सर अत्यधिक रूढ़िवादी (conservative) होता है। कई वास्तविक दुनिया के परिदृश्यों में, जैसे कि टकराव से बचना (collision avoidance), एजेंट सुरक्षा उद्देश्यों को साझा करते हैं (जैसे, कोई भी दुर्घटनाग्रस्त नहीं होना चाहता), जबकि अलग-अलग व्यक्तिगत लक्ष्यों को भी पूरा करते हैं (जैसे, विभिन्न गंतव्यों तक पहुँचना)। शून्य-योग धारणा उन "गैर-शून्य-योग" खेलों में सहयोग की क्षमता को पकड़ने में विफल रहती है, जिससे उन प्रणालियों के लिए सत्यापन विफल हो जाता है जो वास्तव में सुरक्षित हैं। इसके अलावा, मौजूदा गैर-शून्य-योग लॉजिक अक्सर निरंतर गतिकी (continuous dynamics) के साथ संघर्ष करते हैं या जटिल गेम ट्री की आवश्यकता रखते हैं जो अनबाउंडेड डेप्थ वाले हाइब्रिड सिस्टम के लिए अव्यवहार्य होते हैं।

कार्यप्रणाली
यह शोध पत्र अर्ध-प्रतिस्पर्धी विभेदक गेम लॉजिक (dGLsc) प्रस्तुत करता है, जो एक औपचारिक तर्क (formal logic) है जिसे उन हाइब्रिड खेलों को सत्यापित करने के लिए डिज़ाइन किया गया है जहाँ दो खिलाड़ियों (एंजल और डेमन) के पास व्यक्तिगत, संभावित रूप से ओवरलैपिंग लक्ष्य होते हैं। मुख्य कार्यप्रणाली अर्ध-प्रतिस्पर्धात्मकता (semi-competitiveness) की अवधारणा पर आधारित है:

1. व्यवहार मॉडल: खिलाड़ी तब सहयोग करते हैं जब यह दोनों के लिए अपने संबंधित लक्ष्यों को प्राप्त करने में सहायक हो, लेकिन जब आवश्यक हो तो वे प्रतिस्पर्धा करते हैं। विशेष रूप से, एक खिलाड़ी जानबूझकर कभी नहीं हारेगा। यदि कई जीतने वाले विकल्प मौजूद हैं, तो एक खिलाड़ी वह विकल्प चुनता है जो प्रतिद्वंद्वी को जीतने में भी मदद करता है। यदि कोई विकल्प खिलाड़ी के जीतने की ओर नहीं ले जाता है, तो वे प्रतिद्वंद्वी की मदद करने के लिए परोपकारी नहीं होते हैं।
2. सिंटैक्स (Syntax): dGLsc, dGL के सिंटैक्स को मोडैलिटीज को संशोधित करके विस्तारित करता है। $\langle \alpha \rangle P$ (एंजल $P$ तक पहुँचने के लिए $\alpha$ जीतता है) और $[\alpha] Q$ (डेमन $Q$ तक पहुँचने के लिए $\alpha$ जीतता है) के बजाय, dGLsc $\langle \alpha \rangle (P, Q)$ और $[\alpha] (P, Q)$ का उपयोग करता है। ये मोडैलिटीज स्पष्ट रूप से सूत्र के भीतर दोनों खिलाड़ियों के लक्ष्यों को एनकोड करती हैं, जिससे तर्क को व्यक्तिगत उद्देश्यों की परस्पर क्रिया के बारे में सोचने की अनुमति मिलती है।
3. सिमेंटिक्स (Semantics): सिमेंटिक्स एंजल के लिए जीतने वाले क्षेत्रों $\varsigma_\alpha(X, Y)$ और डेमन के लिए $\delta_\alpha(X, Y)$ को परिभाषित करते हैं, जहाँ $X$ और $Y$ लक्ष्य सेट हैं। dGL के विपरीत, ये क्षेत्र पूरक (complementary) नहीं हैं। सिमेंटिक्स सहयोग को शामिल करने के लिए गणना करते हैं जहाँ दोनों खिलाड़ी एक साथ जीत सकते हैं। उदाहरण के लिए, एक निरंतर खेल में, डेमन का जीतने वाला क्षेत्र उन अवस्थाओं को शामिल करता है जहाँ एंजल (जो विकास को नियंत्रित करता है) सिस्टम को एक ऐसे बिंदु पर रोकता है जहाँ दोनों लक्ष्य पूरे हो जाते हैं। पुनरावृत्ति खेलों ($\alpha^*$) के लिए सिमेंटिक्स को फिक्स्पॉइंट्स के माध्यम से परिभाषित किया गया है जो प्रतिस्पर्धी और सहकारी परिदृश्यों के बीच अंतर करते हैं, जिसमें विशिष्टता और मोनोटोनिसिटी सुनिश्चित करने के लिए एंजल के लिए न्यूनतम फिक्स्पॉइंट (least fixpoint) और डेमन के लिए महानतम फिक्स्पॉइंट (greatest fixpoint) का उपयोग किया जाता है।
4. प्रूफ कैलकुलस (Proof Calculus):ic एक सुदृढ़ (sound) और अपेक्षाकृत पूर्ण (relatively complete) प्रमाण कैलकुलस प्रस्तुत किया गया है। इसमें प्रत्येक हाइब्रिड गेम ऑपरेटर (असाइनमेंट, निरंतर विकास, टेस्ट, चॉइस, सीक्वेंस, ड्यूल, रिपिटिशन) के लिए एक्सियम्स शामिल हैं जो दो-लक्ष्य संरचना के अनुरूप हैं। महत्वपूर्ण रूप से, कैलकुलस में एक फिक्स्पॉइंट नियम (FP) शामिल है जो पुनरावृत्ति खेलों को दो न्यूनतम फिक्स्पॉइंट्स (एक प्रतिस्पर्धा के लिए, एक सहयोग के लिए) के संघ (union) के रूप में वर्णित करता है। सिस्टम में एक मोनोटोनिसिटी नियम और एक डिटर्मिनेसी एक्सियम भी शामिल है जो उन मामलों के लिए है जहाँ लक्ष्य पूरक होते हैं।

प्रमुख योगदान

• औपचारिक तर्क dGLsc: निरंतर गतिकी वाले गैर-शून्य-योग हाइब्रिड खेलों के लिए विशेष रूप से डिज़ाइन किए गए एक तर्क का परिचय, जो उन सुरक्षा-महत्वपूर्ण प्रणालियों के सत्यापन को सक्षम बनाता है जहाँ एजेंटों के ओवरलैपिंग लेकिन भिन्न लक्ष्य होते हैं।
• अर्ध-प्रतिस्पर्धी सिमेंटिक्स: एक नवीन सिमेंटिक ढांचा जहाँ खिलाड़ी तभी सहयोग करते हैं जब यह उनकी अपनी सफलता में सहायक हो, जो व्यक्तिगत अनुकूलन और पारस्परिक सुरक्षा के बीच तनाव को बिना किसी स्पष्ट बातचीत प्रोटोकॉल के हल करता है।
• सैद्धांतिक गुण:
  • मोनोटोनिसिटी (Monotonicity): यह सिद्ध किया गया है कि एक खिलाड़ी के लक्ष्य सेट को बढ़ाने से उसका जीतने वाला क्षेत्र विस्तृत हो जाता है।
  • dGL के साथ समानता: प्रदर्शित किया गया है कि जब लक्ष्य पूरक (विरोधी) होते हैं, तो dGLsc मानक शून्य-योग dGL में बदल जाता है।
  • सामान्य समानता: दिखाया गया है कि किसी भी dGLsc जीतने वाले क्षेत्र को रूपांतरित dGL गेम (ड्यूल ऑपरेटर हटाकर) और एक मानक dGL गेम के जीतने वाले क्षेत्रों के वियोजन (disjunction) के रूप में व्यक्त किया जा सकता है, जो इस तर्क की अभिव्यक्तता (expressiveness) को सिद्ध करता है।
• प्रूफ कैलकुलस: एक सुदृढ़ और अपेक्षाकृत पूर्ण कैलकुलस जो गैर-शून्य-योग अवधारणाओं के मैनुअल कोडिंग की आवश्यकता को समाप्त करता है (जिसकी आवश्यकता मानक dGL का उपयोग करने पर होती) और मॉड्यूलर तर्क का समर्थन करता है।

परिणाम
शोध पत्र प्रमाण कैलकुलस की सुदृढ़ता (soundness) स्थापित करता है, यह सुनिश्चित करता है कि सभी सिद्ध सूत्र वैध हैं। यह आगे सापेक्ष पूर्णता (relative completeness) को सिद्ध करता है, जो यह दिखाता है कि dGLsc में कोई भी वैध सूत्र सिद्ध किया जा सकता है यदि अंतर्निहित प्रथम-क्रम तर्क (first-order logic) विभेदक रूप से अभिव्यंजक (differentially expressive) है। शोध पत्र दो विमानों के बीच ईंधन स्टॉक के आदान-प्रदान के एक मानक उदाहरण के माध्यम से dGLsc की उपयोगिता को दर्शाता है। इस परिदृश्य में, मानक dGL सुरक्षा को सत्यापित करने में विफल रहेगा क्योंकि एजेंट एक-दूसरे के लक्ष्य के लिए महत्वपूर्ण चरों (variables) को नियंत्रित नहीं कर सकते हैं। हालाँकि, dGLsc इस परस्पर क्रिया की सुरक्षा को सफलतापूर्वक सत्यापित करता है क्योंकि अर्ध-प्रतिस्पर्धी सिमेंटिक्स एजेंटों को सहयोग करने (जैसे, एंजल द्वारा डेमन का टैंक भरना) की अनुमति देता है ताकि दोनों अपने संबंधित लक्ष्यों तक पहुँच सकें।

महत्व
शोध पत्र का दावा है कि dGLsc गैर-शून्य-योग हाइब्रिड खेलों के बारे में सोचने और तर्क करने का एक स्वाभाविक और सहज तरीका प्रदान करता है, जो मल्टी-एजेंट CPS में प्रचलित हैं लेकिन शून्य-योग धारणाओं के तहत सत्यापित करना कठिन है। अर्ध-प्रतिस्पर्धी व्यवहार को औपचारिक रूप देकर, यह तर्क उन स्थितियों के लिए सुरक्षा प्रमाण सक्षम करता है जो शून्य-योग धारणाओं के तहत असुरक्षित हैं लेकिन वास्तविकता में सहयोग की क्षमता के कारण सुरक्षित हैं। यह कार्य गैर-शून्य-योग साम्यावस्था (equilibria) के गेम-थ्योरेटिक अवधारणाओं और निरंतर गतिकी वाले हाइब्रिड सिस्टम के औपचारिक सत्यापन के बीच के अंतर को पाटता है, जो एक अधिक सटीक उपकरण प्रदान करता है जो प्रतिकूल मॉडलों की तुलना में अधिक सटीक है, फिर भी सामान्य गेम-थ्योरेटिक दृष्टिकोणों की तुलना में गणनात्मक रूप से व्यवहार्य (tractable) है।