तकनीकी सारांश: संभावabilistic समानता दूरी की निरंतरता पर (On the Continuity of the Probabilistic Bisimilarity Distance)

1. समस्या विवरण (Problem Statement)

प्रायोगात्मक द्विसमानता (Probabilistic bisimilarity) लेबल वाले मार्कोव श्रृंखलाओं (LMCs) के लिए एक मानक व्यवहारिक तुल्यता है, जिसका उपयोग स्टेट स्पेस को कम करने और सिस्टम गुणों को सत्यापित करने के लिए किया जाता है। हालाँकि, सटीक द्विसमानता भंगुर (brittle) होती है: ट्रांजिशन प्रोबेबिलिटी में छोटे परिवर्तन भी अवस्थाओं (states) को पूर्णतः असमान बना सकते हैं। इस समस्या को संबोधित करने के लिए, प्रायोगात्मक द्विसमानता दूरी ($\delta_\tau$) को व्यवहारिक अंतर के एक मात्रात्मक माप के रूप में पेश किया गया था, जहाँ $\delta_\tau(s, t) = 0$ तभी होता है जब $s$ और $t$ द्विसमान (bisimilar) हों।

इस मीट्रिक की एक महत्वपूर्ण सीमा इसकी संभावित असततता (discontinuity) है। जैसा कि Jaeger et al. [25] द्वारा उल्लेख किया गया है, ट्रांजिशन प्रोबेबिलिटी में छोटे बदलावों से अवस्थाओं के बीच की दूरी में अचानक, गैर-नगण्य उछाल आ सकता है। निरंतरता का यह अभाव मीट्रिक की अनुप्रयोग क्षमता को कमजोर करता है, विशेषकर उन मॉडलों के लिए जो प्रयोगात्मक डेटा से प्राप्त किए गए हैं, जहाँ ट्रांजिशन प्रोबेबिलिटी अक्सर अनुमानित होती हैं। यदि दूरी असतत है, तो अवस्थाओं को मर्ज करने या मॉडल चेकिंग परिणामों का अनुमान लगाने के लिए इसका उपयोग करना खतरनाक हो सकता है, क्योंकि "प्रतीत होने वाली समानता" अनिश्चितता के प्रति सुदृढ़ (robust) नहीं होगी।

पूर्व कार्य [17] में, लेखकों ने द्विसमान अवस्था युग्मों (bisimilar state pairs) के लिए द्विसमानता दूरी की निरंतरता के लिए एक पर्याप्त स्थिति के रूप में सुदृढ़ प्रायोगात्मक द्विसमानता ($\simeq$) पेश की थी। हालाँकि, दो मौलिक प्रश्न खुले रह गए थे:

1. क्या सुदृढ़ द्विसमानता (robust bisimilarity) निरंतरता के लिए एक आवश्यक स्थिति भी है?
2. गैर-द्विसमान (non-bisimilar) अवस्था युग्मों के लिए निरंतरता को कैसे अभिलक्षणित (characterize) और निर्णय (decide) दिया जा सकता है?

2. कार्यप्रणाली और सैद्धांतिक ढांचा (Methodology and Theoretical Framework)

यह शोध पत्र उत्पाद स्टेट स्पेस $S \times S$ पर कपलिंग्स (couplings) और नीतियों (policies) के सिद्धांतों का विस्तार करके इन प्रश्नों का समाधान करता है।

2.1 प्रारंभिक विवरण (Preliminaries)

लेखक कपलिंग्स (परिभाषा 3) पर आधारित द्विसमानता की मानक परिभाषा का उपयोग करते हैं। द्विसमानता दूरी $\delta_\tau$ को एक फलन $\Delta_\tau$ के न्यूनतम फिक्स्ड पॉइंट (least fixed point) के रूप में परिभाषित किया गया है, जो ट्रांजिशन डिस्ट्रीब्यूशन के सभी कपलिंग्स पर अपेक्षित दूरी को न्यूनतम करता है।
महत्वपूर्ण रूप से, दूरी को नीतियों (परिभाषा 10) के माध्यम से अभिलक्षणित किया जाता है। एक नीति $P$ उत्पाद स्टेट स्पेस $S \times S$ पर एक मार्कोव श्रृंखला प्रेरित करती है। दूरी $\delta_\tau(s, t)$, प्रेरित श्रृंखला में अलग-अलग लेबल वाले युग्मों के सेट ($S^2_1$) तक पहुँचने की न्यूनतम संभावना के अनुरूप होती है (प्रपोजिशन 11)।

2.2 सुदृढ़ द्विसमानता और निरंतरता (Robust Bisimilarity and Continuity)

सुदृढ़ द्विसमानता ($s \simeq t$) को एक ऐसी नीति $P$ के अस्तित्व के रूप में परिभाषित किया गया है जिससे $(s, t)$ से विकर्ण सेट $S^2_\Delta$ (जहाँ अवस्थाएँ समान हैं) तक पहुँचने की संभावना 1 है।

• पूर्व परिणाम (थ्योरम 13): यदि $s \simeq t$, तो $\delta_{(\cdot)}(s, t)$, $\tau$ पर निरंतर है।
• नया योगदान (थ्योरम 14): लेखक इसका विलोम सिद्ध करते हैं: द्विसमान अवस्थाओं ($s \sim t$) के लिए, दूरी फलन की निरंतरता तब बनी रहती है यदि और केवल यदि $s \simeq t$ हो। यह द्विसमान युग्मों के भीतर निरंतरता के लिए सुदृढ़ द्विसमानता को एक आवश्यक और पर्याप्त स्थिति के रूप में स्थापित करता है।

2.3 मनमाने युग्मों के लिए सामान्य अभिलक्षण (General Characterization for Arbitrary Pairs)

यह शोध पत्र विश्लेषण को मनमाने अवस्था युग्मों (गैर-द्विसमान सहित) तक विस्तारित करता है।

• थ्योरम 17: किसी भी $s, t \in S$ के लिए, दूरी फलन $\delta_{(\cdot)}(s, t)$, $\tau$ पर निरंतर है यदि और केवल यदि एक नीति $P$ मौजूद है जिससे $(s, t)$ से $S^2_\Delta$ तक पहुँचने की संभावना ठीक $1 - \delta_\tau(s, t)$ है।
  • यह स्थिति दर्शाती है कि विकर्ण तक पहुँचने में होने वाला "नुकसान" (जो दूरी को 1 तक बढ़ा देगा) दूरी के मान द्वारा ही संतुलित होता है।
  • यदि ऐसी कोई नीति मौजूद नहीं है (अर्थात, विक diagonal तक पहुँचने की अधिकतम संभावना $1 - \delta_\tau(s, t)$ से कम है), तो दूरी असतत है।

2.4 एल्गोरिद्मिक निर्णय प्रक्रिया (Algorithmic Decision Procedure)

थ्योरम 17 के आधार पर, लेखक सभी अवस्था युग्मों के लिए निरंतरता का निर्णय लेने के लिए एल्गोरिदम 1 विकसित करते हैं।

• तंत्र (Mechanism): एल्गोरिदम उन युग्मों के सेट की गणना करता है जो असतत हैं, इसके लिए वह उन युग्मों की पहचान करता है जो "खराब" सेट (वे युग्मा जो द्विसमान तो हैं लेकिन सुदृढ़ नहीं हैं, या वे युग्मा जो अनिवार्य रूप से लेबल मिसमैच की ओर ले जाते हैं) से गुजरे बिना सुदृढ़ सेट तक नहीं पहुँच सकते।
• फिक्स्ड पॉइंट गणना: एल्गोरिदम स्टेट युग्मों के लैटिस (lattice) पर मोनोटोन फलन $A$ और $B$ का उपयोग करता है। यह $\alpha$ (असतत युग्म) के लिए न्यूनतम फिक्स्ड पॉइंट और $\beta$ (निरंतर युग्म) के लिए उच्चतम फिक्स्ड पॉइंट की गणना करता है।
• जटिलता (Complexity): इष्टतम कपलिंग के लिए चेक (एल्गोरिदम 1 की लाइन 6) को न्यूनतम लागत मैक्सिमम फ्लो (minimum cost maximum flow) समस्या में बदल दिया गया है (प्रपोजिशन 25), जिसे बहुपद समय (polynomial time) में हल किया जा सकता है। समग्र एल्गोरिदम स्टेट स्पेस के आकार के सापेक्ष बहुपद समय में चलता है।

3. मुख्य योगदान (Key Contributions)

1. सुदृढ़ द्विसमानता की अनिवार्यता: यह शोध पत्र सिद्ध करता है कि सुदृढ़ द्विसमानता न केवल पर्याप्त है, बल्कि द्विसमान अवस्था युग्मों के लिए द्विसमानता दूरी की निरंतरता के लिए एक आवश्यक शर्त भी है, जिससे [17] के अनुमान को सुलझाया गया।
2. पूर्ण अभिलक्षण: लेखक थ्योरम 17 के माध्यम से सभी अवस्था युग्मों (द्विसमान या नहीं) के लिए निरंतरता का पूर्ण सैद्धांतिक अभिलक्षण प्रदान करते हैं, जो निरंतरता को विकर्ण तक पहुँच को अधिकतम करने वाली एक विशिष्ट नीति से जोड़ता है।
3. बहुपद-समय निर्णय एल्गोरिदम: एक नया एल्गोरिदम प्रस्तुत किया गया है जो सभी अवस्था युग्मों के लिए बहुपद समय में निरंतरता का निर्णय लेता है।
4. प्रयोगात्मक सत्यापन: एल्गोरिदम को PRISM मॉडल चेकर में लागू किया गया। क्वांटिटेटिव वेरिफिकेशन बेंचमार्क सेट (QVBS) और रैंडमाइज्ड जावा एल्गोरिदम (jpf-probabilistic के माध्यम से) पर प्रयोगों से पता चलता है कि निरंतरता तय करने में दूरी की गणना करने की तुलना में न्यूनतम ओवरहेड होता है। कई मामलों में, निरंतरता की जाँच काफी तेज़ है।

4. परिणाम और प्रयोगात्मक मूल्यांकन (Results and Experimental Evaluation)

प्रयोगात्मक मूल्यांकन उन बेंचमार्क पर केंद्रित था जहाँ पारंपरिक द्विसमानता और सुदृढ़ द्विसमानता के तहत संक्षिप्त किए गए मॉडल भिन्न होते हैं (जो संभावित असततता को दर्शाता है)।

• दक्षता (Efficiency): अधिकांश बेंचमार्क के लिए, निरंतरता तय करने में लगने वाला समय द्विसमानता दूरी की गणना करने में लगने वाले समय के बराबर या उससे कम था। उदाहरण के लिए, oscillators बेंचमार्क में, दूरी गणना में ~5 सेकंड लगे, जबकि निरंतरता जाँच में ~0.002 सेकंड लगे।
• तुच्छ मामले (Trivial Cases): जब सभी युग्मों के लिए दूरी निरंतर होती है (जैसे, जब पारंपरिक और सुदृढ़ द्विसमानता एक समान होती है), तो एल्गोरिदम लगभग तुरंत समाप्त हो जाता है।
• व्यावहारिकता: परिणाम पुष्टि करते हैं कि निरंतरता को सत्यापित करने का "अतिरिक्त चरण" कम्प्यूटेशनल रूप से व्यवहार्य है और अनिश्चित ट्रांजिशन प्रोबेबिलिटी वाले मॉडलों के लिए एक सुदृढ़ता गारंटी प्रदान करता है।

5. महत्व और दावे (Significance and Claims)

यह शोध पत्र दावा करता है कि यह प्रायोगात्मक द्विसमानता दूरी की निरंतरता के संबंध में सैद्धांतिक अंतराल को भरता है। सुदृढ़ द्विसमानता को सिद्ध करके और सभी युग्मों के लिए सामान्य अभिलक्षण प्रदान करके, यह कार्य विशेषज्ञों को सक्षम बनाता है:

• सुदृढ़ता का आकलन करना: यह निर्धारित करना कि क्या दो अवस्थाओं के बीच व्यवहारिक समानता ट्रांजिशन प्रोबेबिलिटी के छोटे परिवर्तनों के तहत स्थिर है।
• सुरक्षित मॉडल न्यूनीकरण (Safe Model Reduction): प्रयोगात्मक रूप से प्राप्त मॉडलों में अवस्थाओं को केवल तभी सुरक्षित रूप से मर्ज करना जब निरंतरता सुनिश्चित हो, जिससे "दूरी के उछाल" (distance jumps) के जोखिम से बचा जा सके जो मॉडल चेकिंग परिणामों को अमान्य कर सकते हैं।
• कुशल सत्यापन: निरंतरता जाँच को नगण्य प्रदर्शन लागत के साथ मौजूदा सत्यापन वर्कफ़्लो में एकीकृत करना।

लेखक नोट करते हैं कि जबकि वर्तमान कार्य निर्णायता (decidability) और अभिलक्षण स्थापित करता है, भविष्य के कार्यों का लक्ष्य यह प्रदान करना होगा कि परिवर्तनों के तहत दूरी कितनी बढ़ सकती है और ग्राफ-संरचना-संरक्षण परिवर्तनों के तहत निरंतरता की जांच करना।