On Qualitative Preference in Alternating-time Temporal Logic with Strategy Contexts

तकनीकी सारांश: स्ट्रैटेजी कॉन्टेक्स्ट के साथ अल्टरनेटिंग-टाइम टेम्पोरल लॉजिक में गुणात्मक प्राथमिकता पर

लेखक: डिमिटार पी. गुलेव (Dimitar P. Guelev)
दिनांक: 12 फरवरी, 2026

1. समस्या विवरण

यह शोध पत्र रणनीतिक क्षमता के मौजूदा टेम्पोरल लॉजिक, विशेष रूप से अल्टरनेटिंग-टाइम टेम्पोरल लॉजिक विद स्ट्रैटेजी कॉन्टेक्स्ट्स ($\text{ATL}^*_{sc}$) की एक मौलिक सीमा को संबोधित करता है। जबकि $\text{ATL}^*_{sc}$ नैश इक्विलिब्रियम (Nash equilibrium) जैसे जटिल समाधान अवधारणाओं को व्यक्त करने के लिए पर्याप्त शक्तिशाली है, इसमें विभिन्न परिणामों (plays) के बीच गुणात्मक प्राथमिकता (qualitative preference) के बारे में तर्क करने के लिए कोई मूल तंत्र (native mechanism) नहीं है।

तर्कसंगत गेम थ्योरी (rational game theory) में, खिलाड़ी केवल एक एकल उद्देश्य को संतुष्ट करने की कोशिश नहीं करते; अक्सर उनके पास विभिन्न स्तरों की वांछनीयता के साथ कई उद्देश्य होते हैं। इन प्राथमिकताओं को व्यक्त करने के मौजूदा तरीकों के लिए लॉजिक के बाहर गैर-तुच्छ तर्क (non-trivial reasoning) की आवश्यकता होती है। मुख्य समस्या यह है: $\text{ATL}^*_{sc}$ को एक प्राथमिकता ऑपरेटर और सेकंड-ऑर्डर पाथ क्वांटिफिकेशन (second-order path quantification) शामिल करने के लिए कैसे विस्तारित किया जाए, जिससे लॉजिक अनिर्णायक (undecidable) न हो जाए या इसके लिए पूरी तरह से नए, जटिल मॉडल-चेकिंग एल्गोरिदम की आवश्यकता न पड़े?

2. कार्यप्रणाली

लेखक एक अनुवाद-आधारित दृष्टिकोण (translation-based approach) का उपयोग करते हैं। विस्तारित लॉजिक के लिए एक नया मॉडल-चेकिंग इंजन विकसित करने के बजाय, यह शोध पत्र $\text{ATL}^*_{sc}$ में अभिव्यंजक विशेषताओं को जोड़ने और फिर उन्हें "समाप्त" (eliminate) करने का एक व्यवस्थित तरीका प्रस्तावित करता है, जिससे प्राप्त सूत्रों को स्थापित क्वांटिफाइड कंप्यूटेशन ट्री लॉजिक ($\text{QCTL}^*$) में अनुवादित किया जा सके।

मुख्य कार्यप्रणाली घटक शामिल हैं:

• वरीयता मॉडलिंग (Preference Modeling): प्लेज़ (plays) पर एक बाइनरी प्राथमिकता ऑपरेटर ($<$) पेश किया गया है। एल्गोरिद्मिक व्यवहार्यता सुनिश्चित करने के लिए, लेखक यह मानते हैं कि वरीयता-अस्पष्टता (preference-indiscernibility) (वह गुण जहाँ दो प्लेज़ को खिलाड़ी के वरीयता संबंध द्वारा समान माना जाता है) एक परिमित सूचकांक (finite index) वाला समतुल्य संबंध (equivalence relation) है। इसका अर्थ है कि सभी संभावित प्लेज़ को परिमित संख्या में समतुल्य वर्गों (equivalence classes) में विभाजित किया जा सकता है, जिनमें से प्रत्येक को एक LTL फॉर्मूला द्वारा परिभाषित किया जा सकता है।
• स्ट्रैटेजी एनकोडिंग (Strategy Encoding): रणनीतियों को $\text{QCTL}^*$ फ्रेमवर्क के भीतर क्वांटिफाइड स्टेट वेरिएबल्स का उपयोग करके एनकोड किया गया है।
• स्थिरता धारणा (Stability Assumption): लेखक मानते हैं कि प्राथमिकताएं "स्थिर" (stable) हैं, जिसका अर्थ है कि वे खिलाड़ियों के अपने उद्देश्यों की ओर बढ़ने के साथ अनुमानित रूप से विकसित होती हैं लेकिन अपनी अंतर्निहित संरचना को नहीं बदलती हैं।
• सेकंड-ऑर्डर पाथ क्वांटिफिकेशन: एक विशेष क्वांटिफायर ($\exists_{\sim}$) पेश किया गया है। मानक पाथ क्वांटिफायर्स के विपरीत, जो व्यक्तिगत पथों (paths) पर कार्य करते हैं, $\exists_{\sim}$ पथ वेरिएबल्स को वरीयता-अस्पष्टता के तहत बंद (closed under preference-indiscernibility) प्लेज़ के सेट पर कार्य करने के लिए मजबूर करता है।

3. मुख्य योगदान

1. $\text{ATL}^*_{sc}$ का विस्तार: यह शोध पत्र एक $\text{ATL}^*_{sc,<}$ प्रस्तुत करता है, जो एक बाइनरी प्राथमिकता ऑपरेटर ($<$) और विशेष सेकंड-ऑर्डर पाथ क्वांटिफायर्स ($\exists_{\sim}$ और $\exists_{1}$) वाली $\text{ATL}^*_{sc}$ का विस्तार है।
2. उन्मूलन तकनीकें (Elimination Techniques):
   • वरीयता ऑपरेटर ($<$) को वरीयता समतुल्य वर्गों को परिभाषित करने वाले LTL फॉर्मुलों के एक परिमित संयोजन द्वारा प्रतिस्थापित करके उसे समाप्त करने की एक विधि।
   • विशेष सेकंड-ऑर्डर क्वांटिफायर्स को वरीयता-अस्पष्ट वर्गों के परिमित सेट पर पैरामीटराइज्ड डिसजंक्शंस (parameterized disjunctions) में विस्तारित करके उन्हें समाप्त करने की एक विधि।
3. $\text{QCTL}^*$ के लिए नवीन अनुवाद: लेखक पिछले साहित्य की तुलना में $\text{ATL}^*_{sc}$ से $\text{QCTL}^*$ के लिए एक नया, अधिक कुशल अनुवाद प्रदान करते हैं, जो विशेष रूप से आवश्यक प्रपोजीशनल क्वांटिफिकेशन की संख्या को अनुकूलित करता है।
4. एक्सिओमैटाइजेशन (Axiomatization): शोध पत्र $\text{QCTL}^*_{<}$ में वरीयता ऑपरेटर के लिए एक्सिओम्स का एक सेट प्रदान करता है, जो औपचारिक तर्क (formal reasoning) की सुविधा प्रदान करता है।

4. परिणाम

• समाधान अवधारणाओं की अभिव्यक्तता (Expressivity of Solution Concepts): लेखक यह प्रदर्शित करते हैं कि नैश इक्विलिब्रियम (Nash equilibrium) और सिक्योर इक्विलिब्रियम (secure equilibrium) जैसी जटिल गेम-थ्योरेटिक अवधारणाओं को प्रस्तावित लॉजिक में लगभग शाब्दिक रूप से व्यक्त किया जा सकता है। उदाहरण के लिए, नैश इक्विलिब्रियम को एक एकल $\text{ATL}^*_{sc,<}$ फॉर्मूला के रूप में तैयार किया जा सकता है जो उद्देश्यों की सापेक्ष वांछनीयता को ध्यान में रखता है।
• एल्गोरिद्मिक व्यवहार्यता: यह शोध पत्र सिद्ध करता है कि $\text{ATL}^*_{sc,<}$ के किसी भी फॉर्मूले को $\text{QCTL}^*$ फॉर्मूले में अनुवादित किया जा सकता है। यह सुनिश्चित करता है कि इस नए लॉजिक में मॉडल चेकिंग की समस्या $\text{QCTL}^*$ में ज्ञात निर्णय योग्य (decidable) समस्या में कम की जा सकती है।
• जटिलता प्रबंधन (Complexity Management): LTL फॉर्मुलों के "गार्डेड नॉर्मल फॉर्म" (GNF) का उपयोग करके और क्रियाओं (actions) के एनकोडिंग को अनुकूलित करके, लेखक दिखाते हैं कि अनुवाद गणनात्मक रूप से प्रबंधनीय रहता है, जिससे ऐसे विस्तारों के साथ जुड़े विशिष्ट घातांकीय उछाल (exponential blow-up) से बचा जा सकता है।

5. महत्व

यह कार्य गुणात्मक वरीयता सिद्धांत (qualitative preference theory) और रणनीतिक टेम्पोरल लॉजिक (strategic temporal logic) के बीच के अंतर को पाटता है। इसका महत्व तीन क्षेत्रों में है:

• सैद्धांतिक: यह "तर्कसंगत संश्लेषण" (rational synthesis) के लिए एक औपचारिक, तार्किक ढांचा प्रदान करता है, जहाँ एजेंटों को केवल एक लक्ष्य तक पहुँचने के लिए प्रोग्राम नहीं किया जाता है, बल्कि कई विकल्पों में से सर्वश्रेष्ठ संभव लक्ष्य तक पहुँचने के लिए प्रोग्राम किया जाता है।
• व्यावहारिक: $\text{QCTL}^*$ में अनुवादों पर निर्भर रहकर, लेखक शोधकर्ताओं के लिए एक "प्लग-एंड-प्ले" समाधान प्रदान करते हैं। कोई भी जटिल, वरीयता-जागरूक मल्टीप्लेयर गेम्स के बारे में तर्क करने के लिए मौजूदा $\text{QCTL}^*$ सॉल्वर का उपयोग कर सकता है।
• एकीकृत तर्क (Unified Reasoning): यह दृष्टिकोण वरीयता संबंध के विशिष्ट बीजगणितीय गुणों को "डेटा" के रूप में मानकर विभिन्न समाधान अवधारणाओं (नैश, सिक्योर, डोमिनेंट स्ट्रैटेजी) को संभालने का एक समान तरीका प्रदान करता है।