Complete Supermartingale Certificates for $\omega$-Regular Properties

तकनीकी सारांश: $\omega$-रेगुलर गुणों के लिए पूर्ण सुपरमार्टिंगेल प्रमाणपत्र (Complete Supermartingale Certificates)

समस्या विवरण
यह शोध पत्र सामान्य (संभावित रूप से अनगिनत/uncountable) अवस्था स्थानों (state spaces) पर समय-समान मार्कोव श्रृंखलाओं (time-homogeneous Markov chains) के रूप में मॉडल किए गए संभाव्यता प्रणालियों के औपचारिक सत्यापन (formal verification) को संबोधित करता है। विशेष रूप से, यह रिएक्टिविटी गुणों (reactivity properties) के सत्यापन को लक्षित करता है, जो कि एक ऐसा वर्ग है जो लीनियर टेम्पोरल लॉजिक (LTL) को समाहित करता है और $\omega$-रेगुलर भाषाओं को अभिलक्षित (characterize) करता है। रिएक्टिविटी को स्ट्रीट स्वीकृति स्थितियों (Streett acceptance conditions) के एक परिमित संयोजन के रूप में परिभाषित किया गया है, जहाँ प्रत्येक स्थिति यह आवश्यक करती है कि या तो एक सेट $A$ को परिमित बार (finitely often) देखा जाए या एक सेट $B$ को अनंत बार (infinitely often) देखा जाए ($Fin(A) \cup Inf(B)$)।

यद्यपि लगभग-निश्चित समाप्ति (almost-sure termination) (एक विशिष्ट रिएक्टिविटी गुण) के लिए सुपरमार्टिंगेल प्रमाणपत्रों को सुदृढ़ (sound) और पूर्ण (complete) उपकरण के रूप में स्थापित किया गया है, सामान्य रिएक्टिविटी और $\omega$-रेगुलर गुणों के लिए मौजूदा प्रमाण नियम केवल पर्याप्त स्थितियाँ (sufficient conditions) प्रदान करने की एक गंभीर सीमा से ग्रस्त हैं। फलस्वरूप, ये नियम उन प्रणालियों को प्रमाणित करने में विफल हो सकते हैं जो वास्तव में उस गुण को संतुष्ट करती हैं। पूर्णता के पिछले प्रयास, जो वितरणों (distributions) को व्यक्त करने में सक्षम मान फलनों (value functions) पर निर्भर थे, सत्यापन को कठिन बनाते हैं। यह शोध पत्र ऐसे प्रमाण नियमों का निर्माण करने का प्रयास करता है जो रिएक्टिविटी के लिए सुदृढ़ (sound) और पूर्ण (complete) (विशेष रूप से स्केलर-मान वाले) हों, जो गणनीय अनंत (countably infinite) और सामान्य मापने योग्य (measurable) अवस्था स्थानों पर लागू हो सकें।

कार्यप्रणाली: अवशोषक-क्षेत्र अपघटन (Absorbing-Region Decomposition)
मुख्य तकनीकी योगदान एक ऐसी कार्यप्रणाली है जो किसी भी रिएक्टिविटी गुण को सरल, स्वतंत्र दायित्वों (obligations) के संग्रह में विघटित करती है। यह अपघटन प्रत्येक स्ट्रीट युग्म (Streett pair) $(A_i, B_i)$ के लिए दो प्रकार के क्षेत्रों की पहचान पर आधारित है:

1. एक वैश्विक अपरिवर्तनीय (Global Invariant - $I$): अवस्था स्थान का एक क्षेत्र जिसके भीतर प्रणाली उच्च संभाव्यता के साथ (या लगभग-निश्चित मामले में संभाव्यता 1 के साथ) रहती है।
2. अवशोषक क्षेत्र (Absorbing Regions - $J_i$): प्रत्येक युग्म $i$ के लिए, एक क्षेत्र $J_i \subseteq I \setminus A_i$ जो एक "ट्रैप" (trap) के रूप में कार्य करता है जहाँ $A_i$ पर लौटने की संभाव्यता 1 से कम होती है।

यह अपघटन वैश्विक रिएक्टिविटी गुण के सत्यापन को तीन अलग-अलग प्रकार के दायित्वों में कम करता है:

• गुणात्मक सुरक्षा (Qualitative Safety): यह सुनिश्चित करना कि प्रत्येक $i$ के लिए, $J_i$ से $A_i$ पर लौटने की संभाव्यता 1 से नीचे समान रूप से सीमित (uniformly bounded) है (अर्थात, $J_i$, $A_i$ के संबंध में एक अवशोषक क्षेत्र है)।
• लगभग-निश्चित समाप्ति (Almost-Sure Termination): यह सुनिश्चित करना कि अपरिवर्तनीय $I$ के किसी भी राज्य से, प्रणाली लक्ष्य सेट $B_i$, अवशोषक क्षेत्र $J_i$, और अपरिवर्तनीय $I^c$ के पूरक के संघ (union) में लगभग-निश्चित रूप से समाप्त हो जाती है।
• मात्रात्मक सुरक्षा (Quantitative Safety): इस बात का आधार स्थापित करना कि प्रणाली अपरिवर्तनीय $I$ के भीतर सदैव बनी रहने की संभाव्यता कितनी है।

लेखक सिद्ध करते हैं कि किसी भी समय-समान मार्कोव श्रृंखला के लिए जो रिएक्टिविटी गुण को संतुष्ट करती है, उपयुक्त अवशोषक क्षेत्र और अपरिवर्तनीय हमेशा मौजूद होते हैं। सामान्य मात्रात्मक मामले में, अपरिवर्तनीय का चयन इस प्रकार किया जा सकता है कि इसकी अपरिवर्तनीयता की संभाव्यता किसी भी $\epsilon$ के भीतर रिएक्टिविटी गुण की संभाव्यता के करीब पहुँच जाए। लगभग-निश्चित मामले में, अपरिवर्तनीय का चयन गुण को सटीक रूप से अभिलक्षित करने के लिए किया जा सकता है।

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

1. अपघटन प्रमेय (Decomposition Theorems): यह शोध पत्र स्थापित करता है कि प्रत्येक रिएक्टिविटी गुण गुणात्मक सुरक्षा, लगभग-निश्चित समाप्ति और मात्रात्मक सुरक्षा दायित्वों के एक अपघटन को स्वीकार करता है।

   • प्रमेय 3.7 (सुदृढ़ता/Soundness): यदि एक मार्कोव श्रृंखला एक अपरिवर्तनीय $I$ और विशिष्ट शर्तों को पूरा करने वाले अवशोषक क्षेत्रों $J_i$ को स्वीकार करती है, तो रिएक्टिविटी गुण को संतुष्ट करने की संभाव्यता $I$ में सदैव बने रहने की संभाव्यता के कम से कम बराबर है।
   • प्रमेय 3.12 ($\epsilon$-पूर्णता/$\epsilon$-Completeness): किसी भी रिएक्टिविटी गुण के लिए जिसकी संभाव्यता $p > 0$ है, और किसी भी $\epsilon > 0$ के लिए, एक अपरिवर्तनीय और अवशोषक क्षेत्र मौजूद हैं जिससे अपरिवर्तनीयता की संभाव्यता $p - \epsilon$ के कम से कम बराबर है।
   • प्रमेय 3.14 (लगभग-निश्चित पूर्णता/Almost-Sure Completeness): यदि रिएक्टिविटी गुण लगभग-निश्चित रूप से (संभाव्यता 1) सत्य है, तो एक अपरिवर्तनीय और अवशोषक क्षेत्र मौजूद हैं जिससे अपरिवर्तनीयता की संभाव्यता ठीक 1 है।

2. सुपरमार्टिंगेल प्रमाणपत्रों के साथ इंस्टेंशिएशन (Instantiation with Supermartingale Certificates): लेखक गणनीय अनंत अवस्था स्थानों पर लगभग-निश्चित समाप्ति के लिए मौजूदा सुदृढ़ और पूर्ण प्रमाण नियमों का उपयोग करके इस अपघटन को लागू करते हैं। सुरक्षा और समाप्ति दायित्वों के लिए मानक मात्रात्मक सुरक्षा परिणामों को इनके साथ जोड़कर, वे रिएक्टिविटी के लिए दो नए प्रमाण नियम (प्रमाण नियम #1 और प्रमाण नियम #2) प्राप्त करते हैं।

   • ये नियम सुरक्षा और समाप्ति दायित्वों के लिए स्केलर-मान वाले सुपरमार्टिंगेल प्रमाणपत्रों (मान फलनों) का उपयोग करते हैं।
   • प्रमेय 4.4–4.6 और 4.8–4.10: ये प्रमेय सिद्ध करते हैं कि नए प्रमाण नियम मात्रात्मक रिएक्टिविटी के लिए सुदृढ़ और $\epsilon$-पूर्ण हैं, और लगभग-निश्चित रिएक्टिविटी के लिए पूर्णतः पूर्ण हैं, विशेष रूप से गणनीय अनंत अवस्था स्थानों के लिए।

3. पूर्ववर्ती कार्य का प्रतिवाद (Counterexample to Prior Work): यह शोध पत्र प्रदर्शित करता है कि $\omega$-रेगुलर गुणों के लिए पूर्ववर्ती सुपरमार्टिंगेल प्रमाणपत्र अपूर्ण हैं। "लेंडिंग कैसीनो" (Lending Casino) उदाहरण का उपयोग करते हुए, यह दिखाता है कि एक ऐसी स्थिति जहाँ एक प्रणाली लगभग-निश्चित रूप से एक रिएक्टिविटी गुण को संतुष्ट करती है, लेकिन एक महत्वपूर्ण स्थिति तक पहुँचने का अपेक्षित समय अनंत होता है, जिससे पूर्ववर्ती नियम (जो परिमित अपेक्षित मानों पर निर्भर करते हैं) विफल हो जाते हैं। प्रस्तावित अपघटन सुरक्षा दायित्व (रिटर्न संभाव्यता की सीमा) को समाप्ति दायित्व से अलग करके इस समस्या को संभालता है।

महत्व और दावे
यह शोध पत्र दावा करता है कि यह गणनीय अनंत अवस्था स्थानों वाली समय-समान मार्कोव श्रृंखलाओं के लिए लगभग-निश्चित $\omega$-रेगुलर गुणों के लिए पहले सुदृढ़ और पूर्ण सुपरमार्टिंगेल प्रमाणपत्र और मात्रात्मक $\omega$-रेगुलर गुणों के लिए पहले सुदृढ़ और $\epsilon$-पूर्ण प्रमाणपत्र प्रदान करता है।

इसका महत्व स्टोकेस्टिक विश्लेषण (stochastic analysis) और औपचारिक भाषा सिद्धांत (formal language theory) के बीच के अंतर को पाटने में निहित है। यह सिद्ध करके कि रिएक्टिविटी को समाप्ति और सुरक्षा में विभाजित किया जा सकता है, लेखक स्केलर-मान वाले प्रमाणपत्रों की मौजूदा तकनीकों का उपयोग करके जटिल $\omega$-रेगुलर गुणों के सत्यापन को स्वचालित करने में सक्षम बनाते हैं। लेखक यह भी उल्लेख करते हैं कि यद्यपि उनकी पूर्णता गारंटी वर्तमान में गणनीय अनंत अवस्था स्थानों पर लागू होती है, लेकिन अंतर्निहित अपघटन रणनीति सामान्य अवस्था स्थानों के लिए भी मान्य है, जो यह सुझाव देती है कि सामान्य स्थानों पर लगभग-निश्चित समाप्ति को प्रमाणित करने की समस्या तक विस्तार करना पूर्णता को विस्तारित करना है। यह कार्य इन प्रमाणपत्रों के स्वतः निर्माण (synthesis) को हल करने का दावा नहीं करता है, बल्कि उसके लिए सैद्धांतिक आधार प्रदान करता है।