तकनीकी सारांश: रिएक्टिव सिस्टम में स्वतंत्र वेरिएबल सेट्स की पहचान करने के लिए एक सही एल्गोरिदम

समस्या विवरण

रिएक्टिव सिंथेसिस (Reactive synthesis), जो सभी संभावित वातावरण व्यवहारों के विरुद्ध लीनियर टेम्पोरल लॉजिक (LTL) विशिष्टताओं को संतुष्ट करने वाले सिस्टम का स्वचालित निर्माण है, एक गणनात्मक रूप से कठिन समस्या है (2EXPTIME-complete)। स्केलेबिलिटी को संबोधित करने के लिए, एक सामान्य रणनीति जटिल विशिष्टता को छोटे, स्वतंत्र उप-विशिष्टताओं (subspecifications) में विभाजित करना है जिन्हें अलग से हल किया जा सके।

यह शोध पत्र Iannopollo (2018) और Iannopollo et al. (2024) द्वारा प्रस्तुत DecomposeContract (DC) एल्गोरिदम की समीक्षा करता है। यह एल्गोरिदम एक मॉडल चेकर का उपयोग करके सिस्टम-नियंत्रित वेरिएबल्स के उन सेट्स की पहचान करता है जो एक LTL फॉर्मूला के भीतर स्वतंत्र रूप से व्यवहार करते हैं। जबकि मूल DC एल्गोरिदम साउंड (sound) है (कोई भी सेट जिसे यह स्वतंत्र के रूप में पहचानता है, वह वास्तव में स्वतंत्र है), लेकिन यह पूर्ण (complete) नहीं है। यह सूक्ष्म विभाजनों का पता लगाने में विफल हो सकता है, और स्वतंत्र वेरिएबल्स के छोटे विभाजन के बजाय वेरिएबल्स का एक ही बड़ा सेट वापस कर सकता है। यह सीमा संश्लेषण (synthesis) की स्केलेबिलिटी में सुधार के लिए अपघटन (decomposition) के पूर्ण दोहन को बाधित करती है।

कार्यप्रणाली और सिमेंटिक आधार

1. स्वतंत्रता का सिमेंटिक विश्लेषण

लेखक DC में उपयोग किए गए स्वतंत्रता के विचार का एक कठोर सिमेंटिक विश्लेषण प्रदान करते हैं। वे ट्रेस (trace) के सेट्स पर लागू प्रोजेक्शन (projection) और जॉइन (join) ऑपरेटरों, विशेष रूप से रिलेशनल अलजेब्रा की अवधारणाओं का उपयोग करके स्वतंत्रता को औपचारिक रूप देते हैं।

• ट्रेस प्रोजेक्शन ($\sigma \upharpoonright V$): वातावरण वेरिएबल्स को सुरक्षित रखते हुए एक ट्रेस को वेरिएबल्स के उपसमूह $V$ तक सीमित करता है।
• जॉइन ($\Sigma_1 \bowtie \Sigma_2$): विभिन्न वेरिएबल उपसमूहों पर ट्रेस के सेट्स को उनके यूनियन पर ट्रेस के सेट्स में संयोजित करता है, बशर्ते कि ट्रेस प्रतिच्छेदन (intersection) पर सहमत हों।
• जॉइन-स्वतंत्रता (Join-Independence): सिस्टम वेरिएबल्स का एक सेट $V \subseteq O$ एक फॉर्मूला $\phi$ में स्वतंत्र तब कहलाता है यदि और केवल यदि $V$ और उसके पूरक $\bar{V}$ पर मॉडल सेट $\Sigma_\phi$ के प्रोजेक्शन का जॉइन मूल मॉडल सेट को पुनर्गठित करता है:
  $$(\Sigma_\phi \upharpoonright V) \bowtie (\Sigma_\phi \upharpoonright \bar{V}) = \Sigma_\phi$$
  लेखक सिद्ध करते हैं कि यह सिमेंटिक परिभाषा मूल DC एल्गोरिदम में उपयोग की जाने वाली सिंटैक्टिक वैधता स्थिति के समकक्ष है: $(\phi_V \land \phi_{\bar{V}}) \to \phi$ वैध है।

2. मूल DC एल्गोरिदम की सीमा

मूल DC एल्गोरिदम स्वतंत्र सेट्स को वृद्धिशील (incrementally) रूप से बनाता है। एक एकल वेरिएबल से शुरू करते हुए, यह जांचता है कि क्या वर्तमान सेट $V$ स्वतंत्र है। यदि वैधता जांच विफल हो जाती है, तो मॉडल चेकर एक काउंटरएग्जांपल ट्रेस लौटाता है। एल्गोरिदम फिर इस ट्रेस का विश्लेषण करता है ताकि उन वेरिएबल्स को खोजा जा सके जिनके मान प्रोजेक्शन में उनके "प्राइम्ड" (fresh) समकक्षों से भिन्न हैं, और उन्हें $V$ में जोड़ देता है।

शोध पत्र यह प्रदर्शित करता है कि यह दृष्टिकोण अपूर्ण है क्योंकि यह वर्तमान सेट और शेष वेरिएबल्स के बीच सीधे चेक पर निर्भर करता है। यह मध्यस्थ निर्भरताओं (mediated dependencies) को ध्यान में रखने में विफल रहता है। जैसा कि उदाहरण 11 में दिखाया गया है, एक वेरिएबल $b$ केवल तभी एक सेट पर निर्भर हो सकता है जब उसे तीसरे वेरिएबल $a$ के साथ माना जाए, भले ही $b$ और शेष सेट के बीच सीधा इंटरैक्शन इस निर्भरता को तुरंत प्रकट न करे। फलस्वरूप, DC समय से पहले एक सेट को स्वतंत्र मान सकता है या आवश्यक वेरिएबल्स को मर्ज करने में विफल हो सकता है, जिससे गैर-न्यूनतम (non-minimal) स्वतंत्र सेट्स प्राप्त होते हैं।

3. प्रस्तावित समाधान: NDC एल्गोरिदम

पूर्णता प्राप्त करने के लिए, लेखक NDC (New DecomposeContract) प्रस्तावित करते हैं। मुख्य संशोधन ParseTrace फंक्शन में है, जिसे NewParseTrace द्वारा प्रतिस्थापित किया गया है।

• परिष्कृत निर्भरता पहचान (Refined Dependency Detection): जब वैधता जांच विफल होती है, तो NewParseTrace केवल काउंटरए एग्जांपल में भिन्न होने वाले सभी वेरिएबल्स को नहीं जोड़ता है। इसके बजाय, यह पुनरावृत्ति (iteratively) से एक फॉर्मूला binds का निर्माण करता है जो निर्भर पाए गए वेरिएबल्स पर बाधाओं ($\Diamond(z \leftrightarrow \neg z')$) को संचित करता है।
• पुनरावृत्ति परिशोधन (Iterative Refinement): एल्गोरिदम एक विखंड़ (disjunction) के साथ मॉडल चेकर को क्वेरी करता है: binds $\lor$ ((\phi_V \land \phi_{\bar{V}}) \to \phi). यदि यह फॉर्मूला अमान्य है, तो मॉडल चेकर एक नया ट्रेस प्रदान करता है जहाँ वर्तमान binds बाधाओं का उल्लंघन होता है, जिससे एक नया वेरिएबल $z$ प्रकट होता है जिसे सेट में जोड़ा जाना चाहिए।
• सैद्धांतिक गारंटी: एल्गोरिदम लेम्मा 6 पर निर्भर करता है, जो यह स्थापित करता है कि यदि एक सेट $V$ एक बड़े स्वतंत्र सुपरसेट $W$ के भीतर निर्भर है, तो कोई भी वेरिएबल $q \in W$ तब तक स्वतंत्रता को "साक्षी" (witness) नहीं बना सकता जब तक कि निर्भरता को बाधाओं के संचय के माध्यम से स्पष्ट रूप से उजागर न किया जाए। यह सुनिश्चित करता है कि एल्गोरिदम सेट का विस्तार तब तक करता रहता है जब तक कि वह एक न्यूनतम स्वतंत्र सेट तक नहीं पहुँच जाता।

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

1. गणितीय औपचारिकता: यह शोध पत्र Iannopollo के कार्य में उपयोग किए गए स्वतंत्रता के विचार का पहला कठोर सिमेंटिक विवरण प्रदान करता है, जिसे ट्रेस प्रोजेक्शन और जॉइन के माध्यम से परिभाषित किया गया है। यह अपघटन पद्धति के सैद्धांतिक आधार को स्पष्ट करता है।
2. अपूर्णता का प्रमाण: लेखक एक ठोस काउंटरएग्जांपल (उदाहरण 6 और उदाहरण 11) प्रस्तुत करते हैं जो प्रदर्शित करता है कि मूल DC एल्गोरिदम पूर्ण नहीं है और वैध विभाजनों को पहचानने में विफल हो सकता है।
3. सही और पूर्ण एल्गोरिदम (NDC): शोध पत्र NDC पेश करता है, जो एक परिष्कृत एल्गोरिदम है जो (मॉडल चेकर की लागत को छोड़कर) मूल विधि की बहुपद-समय (polynomial-time) प्रकृति को बनाए रखते हुए पूर्णता सुनिश्चित करता है।
4. न्यूनतमता गारंटी (Minimality Guarantee): प्राथमिक सैद्धांतिक परिणाम (थ्योरम 1) यह सिद्ध करता है कि NDC सिस्टम वेरिएबल्स को न्यूनतम स्वतंत्र सेट्स में विभाजित करता है। इसका अर्थ है कि यदि एक सेट को स्वतंत्र के रूप में लौटाया जाता है, तो उसका कोई भी गैर-रिक्त उचित उपसमूह (non-empty proper subset) स्वयं स्वतंत्र नहीं है। यह मूल DC की तुलना में एक मजबूत गारंटी है, जो केवल साउंडनेस की गारंटी देता है।
5. वास्तविकता (Realisability) में सीमाएँ: शोध पत्र संतुष्टि (satisfiability - जहाँ ट्रेस सिमेंटिक ऑब्जेक्ट हैं) और वास्तविकता (realisability - जहाँ जीतने वाली रणनीतियाँ सिमेंटिक ऑब्जेक्ट हैं) के बीच स्पष्ट रूप से अंतर करता है। लेखक नोट करते हैं कि जबकि NDC संतुष्टि सेटिंग में स्वतंत्रता की पहचान करने के लिए पूर्ण है, इन परिणामों को वास्तविकता सेटिंग में विस्तारित करना काफी चुनौतीपूर्ण है। वास्तविकता सेटिंग में, जीतने वाली रणनीतियों द्वारा प्रेरित ट्रेसों का सेट सभी संतुष्ट करने वाले ट्रेसों का एक उपसमुच्चय है, और अपघटन की न्यूनतमता की गारंटी संतुष्टि-आधारित दृष्टिकोण की तरह कुशलता से कंप्यूट करने योग्य नहीं है।

महत्व और दावे

शोध पत्र का दावा है कि इसका मुख्य योगदान सैद्धांतिक है, जो रिएक्टिव सिंथेसिस में अपघटन विधियों के लिए एक कठोर आधार प्रदान करता है। स्वतंत्रता के अर्थ को स्पष्ट करके और एल्गोरिथम प्रक्रिया को सुधारकर, लेखक LTL विशिष्टताओं को न्यूनतम स्वतंत्र घटकों में विभाजित करने के लिए विश्वसनीय अपघटन को सक्षम करते हैं।

इसका महत्व निम्नलिखित में निहित है:

• सटीकता (Correctness): यह सुनिश्चित करना कि अपघटन विशिष्टताओं को विभाजित करने के अवसरों को नहीं चूकता है, जो सिंथेसिस टूल्स की स्केलेबिलिटी के लिए महत्वपूर्ण है।
• दक्षता (Efficiency): ऑटोमेटा-थ्योरेटिक ऑपरेशन्स जैसे कॉम्प्लीमेंटेशन (complementation) के महंगे उपयोग के बजाय मॉडल चेकर्स (जो अत्यधिक अनुकूलित हैं) का उपयोग करने की व्यावहारिक दक्षता को बनाए रखना।
• स्पष्टता (Clarity): विधि की सीमाओं को स्पष्ट रूप से रेखांकित करना, विशेष रूप से संतुष्टि-आधारित स्वतंत्रता और रणनीति-आधारित स्वतंत्रता के बीच अंतर करना, ताकि पूर्ण वास्तविकता समस्या पर इन परिणामों के प्रत्यक्ष अनुप्रयोग के संबंध में अति-आशावादी अपेक्षाओं को रोका जा सके।

यह कार्य नए प्रायोगिक बेंचमार्क या भविष्य के टूल कार्यान्वयन का प्रस्ताव नहीं करता है बल्कि स्वयं अपघटन तर्क की गणितीय शुद्धता और पूर्णता को स्थापित करने पर ध्यान केंद्रित करता है।