A Bitopological Approach to Finite Reduction and Bounded Exact-Value Certificates for Fitting's Finite Heyting-valued Modal Logic

तकनीकी सारांश: फिटिंग के परिमित हेयटिंग-मानed (Heyting-valued) मोडल लॉजिक के लिए फाइनाइट रिडक्शन और बाउंडेड एक्ज़ैक्ट-वैल्यू सर्टिफिकेट हेतु एक बिटोपोलॉजिकल दृष्टिकोण

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

यह शोध पत्र फिटिंग के परिमित हेयटिंग-मानed मोडल लॉजिक के भीतर परिमित-अवस्था न्यूनीकरण (finite-state reduction) और प्रति-उदाहरण निष्कर्षण (counterexample extraction) की समस्या को संबोधित करता है। इस तर्क में, सूत्र (formulas) बाइनरी बूलियन बीजगणित के बजाय एक निश्चित परिमित हेयिंग बीजगणित $L$ के सत्य मानों को ग्रहण करते हैं। आवश्यकता ऑपरेटर $\Box$ की व्याख्या सुलभ अवस्थाओं (accessible states) पर सत्य मानों के इन्फिमम (infimum/meet) के रूप में की जाती है।

मुख्य चुनौती दोहरी है:

1. अवस्था न्यूनीकरण (State Reduction): एक परिमित $L$-मानed क्रिपके मॉडल $M = (W, R, V)$ और एक परिमित प्रपोज़िशनल शब्दावली $\Sigma$ दिए जाने पर, हम एक ऐसा न्यूनीकृत मॉडल कैसे बना सकते हैं जो $\Sigma$ के प्रत्येक सूत्र के सटीक सत्य मान (exact truth value) को सुरक्षित रखे? शास्त्रीय मॉडल चेकिंग के विपरीत, जहाँ केवल वैधता (सत्य मान 1) महत्वपूर्ण होती है, बहु-मान (many-valued) सत्यापन में मध्यवर्ती सत्य मानों (जैसे अनिश्चितता या आंशिक सत्य) को संरक्षित करना आवश्यक होता है।
2. प्रमाणपत्र निर्माण (Certificate Construction): एक विशिष्ट सूत्र $\phi$ और अवस्था $x$ के लिए जहाँ $\phi$ विफल होता है (अर्थात $J\phi K_M(x) \neq 1$), क्या एक परिमित, वृक्ष-समान प्रति-उदाहरण (tree-like counterexample) का निर्माण किया जा सकता है जिसका आकार मूल मॉडल के स्टेट स्पेस से स्वतंत्र हो, और जो केवल बीजगणित $L$ और $\phi$ की वाक्य रचना (syntax) पर निर्भर हो?

मौजूदा विधियाँ, जैसे कि फिल्ट्रेशन या पार्टिशन रिफाइनमेंट, अक्सर बूलियन वैधता पर ध्यान केंद्रित करती हैं या सटीक-मान संरक्षण के लिए बिटोपोलॉजिकल द्वैत (bitopological duality) का स्पष्ट रूप से उपयोग नहीं करती हैं।

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

लेखक एक संबंधपरक बिटोपोलॉजिकल प्रतिनिधित्व (relational bitopological representation) का उपयोग करते हैं जो बीजगणितीय लैट्टिस-मानed मोडल बीजगणितों के द्वैत सिद्धांत से व्युत्पन्न है। कार्यप्रणाली दो मुख्य चरणों में आगे बढ़ती है:

A. बिटोपोलॉजिकल प्रतिनिधित्व और द्वैत (Duality)
यह शोध पत्र $L$-ML-बीजगणितों (एक परिमित हेयिंग बीजगणित पर आधारित मोडल बीजगणित) की श्रेणी और संबंधपरक युग्म बूलियन स्थानों ($PRBS_L$) के बीच द्वैत का उपयोग करता है।

• द्वैत स्थान (Dual Space): एक बीजगणित $A$ के लिए, द्वैत स्थान दो टोपोलॉजी ($\tau_1, \tau_2$) और एक कैनोनिकल बाइनरी संबंध $R_A$ के साथ $X_A = \text{Hom}_{VAL}(A, L)$ का समुच्चय है।
• कैनोनिकल संबंध: संबंध $R_A$ को इस प्रकार परिभाषित किया गया है कि $h R_A k$ तब होता है जब सभी $a \in A$ के लिए $h(\Box a) \leq k(a)$ हो। यह संबंध द्वैत स्थान में मोडल अर्थ विज्ञान (semantics) को कैप्चर करता है।
• प्रतिनिधित्व प्रमेय: शोध पत्र यह स्थापित करता है कि श्रेणी $L$-ML-बीजगणितों, $PRBS_L$ के साथ द्वैत रूप से समतुल्य है, जो यह सुनिश्चित करता है कि बीजगणितीय संचालन टोपोलॉजिकल और संबंधपरक संरचनाओं के अनुरूप हैं।

B. अवलोकनात्मक तुल्यता के माध्यम से परिमित न्यूनीकरण
एक परिमित मॉडल $M$ और शब्दावली $\Sigma$ के लिए, लेखक एक मोडल ऑब्जर्वेशन बीजगणित $A^\Sigma_M$ को परिभाषित करते हैं, जो $\Sigma$ के लिए परमाणु मूल्यांकनों (atomic valuations) $V(p)$ द्वारा जनित होता है।

• मूल्यांकन मानचित्र (Evaluation Map): एक मानचित्र $\eta^\Sigma_M: W \to X_{A^\Sigma_M}$ को $\eta^\Sigma_M(x)(f) = f(x)$ द्वारा परिभाषित किया जाता है।
• अवलोकनात्मक तुल्यता (Observational Equivalence): दो अवस्थाएँ $x, y$ तुल्य हैं ($x \equiv^\Sigma_M y$) यदि वे जनित बीजगणित के प्रत्येक सूत्र के लिए समान सत्य मान प्रदान करती हैं।
• कोशिएंट निर्माण (Quotient Construction): न्यूनीकृत मॉडल का निर्माण भागफल (quotient) $W / \equiv^\Sigma_M$ के रूप में किया जाता है। लेखक सिद्ध करते हैं कि यह भागफल बिटोपोलॉजिकल द्वैत के भीतर परिमित छवि $X^\Sigma_M = \eta^\Sigma_M[W]$ के समांग (isomorphic) है। महत्वपूर्ण रूप से, न्यूनीकृत मॉडल पर संक्रमण संबंध (transition relation) को $R_{A^\Sigma_M}$ के प्रतिबंध के रूप में दिखाया गया है।

C. बाउंडेड सर्टिफिकेट निर्माण
प्रति-उदाहरण निष्कर्षण को संबोधित करने के लिए, लेखक हेयिंग बीजगणक $L$ की परिमित ऊँचाई $h(L)$ का उपयोग करते हैं।

• मीट संपीड़न (Meet Compression): एक लेम्मा सिद्ध करता है कि $S \subseteq L$ के किसी भी उपसमुच्चय के मीट (meet) को एक उपसमुच्चय $S_0 \subseteq S$ द्वारा संरक्षित किया जा सकता है जहाँ $|S_0| \leq h(L) - 1$ है।
• वृक्ष निर्माण (Tree Construction): सूत्र $\phi$ के मोडल गहराई $d$ और अवस्था $x$ के लिए, एक वृक्ष-समान मॉडल $C(M, x, \phi)$ का निर्माण किया जाता है। प्रत्येक नोड पर, केवल आवश्यक संख्या में उत्तराधिकारियों (successors) को रखा जाता है (विशेष रूप से, वे जो प्रत्येक $\Box$-उपसूत्र के लिए मीट को संरक्षित करने के लिए आवश्यक हैं)।
• आकार सीमा (Size Bounds): ब्रांचिंग फैक्टर को $(h(L) - 1) \times m_\Box(\phi)$ द्वारा सीमित किया गया है, जहाँ $m_\Box(\phi)$ अलग-अलग बॉक्स्ड उपसूत्रों की संख्या है। कुल आकार मूल मॉडल के आकार से स्वतंत्र है।

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

1. अवलोकनात्मक भागफल और द्वैत छवि का समांगता (Isomorphism)
प्राथमिक सैद्धांतिक परिणाम यह है कि एक परिमित फिटिंग मॉडल का अवलोकनात्मक भागफल, उसके जनित ऑब्जर्वेशन बीजगणित के द्वैत स्थान में मॉडल की परिमित छवि के समांग है।

• सटीक मान संरक्षण: न्यूनीकरण $\Sigma$ पर प्रत्येक सूत्र के सटीक सत्य मान को सुरक्षित रखता है, न कि केवल वैधता को। किसी भी $\phi \in \text{Form}(\Sigma)$ और अवस्था $x$ के लिए, $J\phi K_{M^{red}}([x]) = J\phi K_M(x)$।
• न्यूनतमता (Minimality): यह भागफल उस न्यूनतम भागफल है जिसके माध्यम से सभी जनित अवलोकन फैक्टराइज़ होते हैं। यदि कोई अन्य सर्जेक्टिव मैप $h: W \to Y$ $\Sigma$ के सभी सूत्रों के सटीक मानों को संरक्षित करता है, तो $|W/\equiv^\Sigma_M| \leq |Y|$।

2. बाउंडेड एक्ज़ैक्ट-वैल्यू सर्टिफिकेट्स
यह शोध पत्र किसी भी सूत्र $\phi$ और अवस्था $x$ के लिए एक परिमित वृक्ष-समान प्रमाण पत्र $C(M, x, \phi)$ का निर्माण करता है।

• सीमाबद्धता (Boundedness): वृक्ष की गहराई $\phi$ की मोडल गहराई द्वारा सीमित है, और ब्रांचिंग $(h(L)-1)m_\Box(\phi)$ द्वारा सीमित है।
• प्रति-उदाहरण निष्कर्षण: यदि $J\phi K_M(x) \neq 1$, तो प्रमाण पत्र (और उसका बाद का अवलोकनात्मक न्यूनीकरण) सटीक विफलता मान को संरक्षित करने वाला एक परिमित पॉइंटेड प्रति-उदाहरण प्रदान करता है। इस प्रमाण पत्र का आकार $M$ के आकार पर नहीं, बल्कि केवल $L$ और $\phi$ की वाक्य रचना पर निर्भर करता है।

3. परिमित निर्माण प्रक्रिया
शोध पत्र एक प्रभावी परिमित प्रक्रिया को रेखांकित करता है जिसके द्वारा ऑब्जर्वेशन बीजगणित को पुनरावृत्ति (iteratively) से उत्पन्न करके और समान मूल्यांकन वेक्टर वाले राज्यों को समूहबद्ध करके न्यूनीकृत मॉडल की गणना की जा सकती है।

4. महत्व और दावे

यह शोध पत्र निम्नलिखित क्षेत्रों में अपने महत्व का दावा करता है, व्यापक सत्यापन समस्याओं के सापेक्ष एक मध्यम दायरे को बनाए रखते हुए:

• विशिष्ट परिमित न्यूनीकरण: यह कार्य बिटोपोलॉजिकल द्वैत का उपयोग करके फिटिंग के तर्क के लिए परिमित न्यूनीकरण समस्या का एक विशिष्ट समाधान प्रदान करता है। यह स्पष्ट करता है कि न्यूनीकृत मॉडल एक मनमाना भागफल नहीं है, बल्कि द्वैत स्थान में संबंधपरक छवि के रूप में संरचनात्मक रूप से पुनः प्राप्त किया गया है।
• मध्यवर्ती मानों का संरक्षण: कई न्यूनीकरण तकनीकों के विपरीत जो बूलियन वैधता पर ध्यान केंद्रित करती हैं, यह दृष्टिकोण संपूर्ण लैट्टिस (lattice) के सत्य मानों को संरक्षित करना सुनिश्चित करता है, जो ग्रेडेड, अपूर्ण या अनिश्चित सूचना प्रणालियों के लिए महत्वपूर्ण है।
• सूत्र-निर्भर सीमाएँ: सर्टिफिकेट प्रमेय प्रति-उदाहरण के लिए एक आकार सीमा प्रदान करता है जो सिस्टम के आकार से स्वतंत्र है। यह बहु-मान मॉडल चेकिंग के लिए एक महत्वपूर्ण सैद्धांतिक प्रगति है, क्योंकि यह गारंटी देता है कि प्रति-उदाहरणों को निकाले जाने की जटिलता केवल तर्क के बीजगणितीय ऊँचाई और सूत्र की संरचना पर निर्भर करती है।
• सामान्य द्वैत से अंतर: लेखक स्पष्ट रूप से कहते हैं कि यह शोध पत्र एक नया सामान्य द्वैत सिद्धांत प्रस्तावित नहीं करता है। इसके बजाय, यह एक विशिष्ट न्यूनीकरण समस्या को हल करने और सटीक-मान संरक्षण गुणों को स्थापित करने के लिए मौजूदा संबंधपरक बिटोपोलॉजिकल निरूपणों का लाभ उठाता है।

शोध पत्र यह नोट करते हुए समाप्त होता है कि जबकि 'मीट संपीड़न' तर्क $L$ की परिमित ऊँचाई पर निर्भर करता है, अनंत ऊँचाई वाले फजी कोएल्जेब्रिक मॉडलों तक इन परिणामों का विस्तार करना एक खुला प्रश्न बना हुआ है।