Value Functions for Temporal Logic: Optimal Policies and Safety Filters

तकनीकी सारांश: टेम्पोरल लॉजिक के लिए वैल्यू फंक्शन्स: इष्टतम नीतियां और सुरक्षा फिल्टर

समस्या विवरण
यद्यपि बुनियादी रीच (reach), अवॉयड (avoid), और रीच-अवॉयड (reach-avoid) समस्याओं के लिए बेलमैन समीकरण अच्छी तरह से स्थापित हैं, फिर भी अनडिस्काउंटेड अनंत-क्षितिज (undiscounted infinite-horizon) सेटिंग्स में, विशेष रूप से जटिल टेम्पोरल लॉजिक (TL) विनिर्देशों के लिए, वैल्यू ऑप्टिमलिटी और पॉलिसी ऑप्टिमलिटी के बीच का संबंध सूक्ष्म हो जाता है। एक महत्वपूर्ण पैथोलॉजी (pathology) उत्पन्न होती है जहाँ Q-फंक्शन को लालची तरीके से (greedily) अधिकतम करने से ऐसी नीतियां बन सकती हैं जो रीच-अवॉयड समस्याओं (जो Until विनिर्देशों के समकक्ष हैं) के लिए कार्य पूरा करने को अनिश्चित काल के लिए टाल देती हैं, भले ही वैल्यू फंक्शन स्वयं इष्टतम हो। यह इसलिए होता है क्योंकि अनंत प्रक्षेप पथों (infinite trajectories) के लिए इष्टतम क्रिया अनुक्रम मौलिक रूप से नॉन-मार्कोवियन (non-Markovian) होता है; शेष अनंत-क्षितिज विनिर्देशों को संतुष्ट करने के लिए इष्टतम इनपुट को वर्तमान वैल्यू को अधिकतम करने से बदलकर एक घटक वैल्यू (constituent value) में "स्विच" करने की आवश्यकता हो सकती है। मौजूदा विधियाँ, जैसे कि दोहरे-उद्देश्य वाले समस्याओं के लिए स्टेट-अगमेंटेशन (state-augmentation), नेस्टेड Until, Globally, और Globally-Until विनिर्देशों वाले जटिल सूत्रों में सामान्यीकरण करने में संघर्ष करती हैं। इसके अलावा, एक ऐसे सुरक्षा फिल्टर (safety filter) की आवश्यकता है जो सरल अवॉयड या रीच-अवॉयड कार्यों से आगे बढ़कर जटिल TL विनिर्देशों की संतुष्टि सुनिश्चित कर सके।

कार्यप्रणाली (Methodology)
लेखक समस्या की नॉन-मार्कोवियन प्रकृति को संभालने के लिए स्टेट हिस्ट्रीज़ (state histories) तक वैल्यू और Q-फंक्शन्स को सामान्यीकृत करने वाले एक ढांचे का प्रस्ताव करते हैं। कार्यप्रणाली एक ग्राफ में घटक वैल्यू फंक्शन्स के लिए TL के वैल्यू फंक्शन के बीजगणितीय अपघटन (algebraic decomposition) पर निर्भर करती है।

1. नॉन-मार्कोवियन वैल्यू फंक्शन्स: पेपर केवल वर्तमान अवस्थाओं के बजाय स्टेट हिस्ट्रीज़ $x_{0:t}$ पर इष्टतम वैल्यू फंक्शन $V^*$ और Q-फंक्शन्स $Q$ को परिभाषित करता है। यह नीति को उन हिस्टरीज को ध्यान में रखने की अनुमति देता है जो टेम्पोरल बाधाओं को संतुष्ट करने के लिए आवश्यक हैं।
2. टाइम-अगमेंटेड सिस्टम और विटनेस टाइम्स: Until ($U$) विनिर्देशों में होने वाली टालने (deferral) की समस्या को संबोधित करने के लिए, लेखक एक टाइमर के साथ एक टाइम-अगमेंटेड सिस्टम पेश करते हैं। वे एक "इष्टतम विटनेस टाइम" $\sigma^*$ को परिभाषित करते हैं, जो वह प्रारंभिक समय है जब एक प्रक्षेप पथ इष्टतम रोबस्टनेस स्कोर प्राप्त करता है। यह ऐसी नीतियां बनाने की अनुमति देता है जो एक परिमित-क्षितिज लालची रणनीति (विटनेस टाइम के भीतर Q-फंक्शन को अधिकतम करना) से एक सफिक्स पॉलिसी (suffix policy) में स्विच करती है जो शेष उप-सूत्र (sub-formula) को संतुष्ट करती है।
3. कंपोजिशनल पॉलिसी निर्माण: पेपर टेम्पोरल लॉजिक के एक विशिष्ट खंड (परिभाषा 3) के लिए इष्टतम नीतियां निर्मित करता है, जिसमें शामिल हैं:
   • प्रोपोज़िशनल फॉर्मुला (Propositional formulas)।
   • Until ($p U \phi$), Next ($X\phi$), और Globally ($Gp$) ऑपरेटर्स।
   • Globally-Until ($G(\bigvee p_i U r_i)$), जो बुची एक्सेप्टेंस क्राइटेरिया (Büchi acceptance criteria) को एनकोड करता है।
   • डिसजंक्शन्स (disjunctions) और प्रोपोज़िशनल कंजंक्शन्स (conjunctions)।
     निर्माण यह मानता है कि उप-सूत्रों के लिए इष्टतम नीतियां मौजूद हैं (धारणा 2) और उन्हें पुनरावर्ती रूप से (recursively) जोड़ता है। Globally-Until के लिए, नीति अनंत दौरों को सुनिश्चित करने के लिए अनुक्रम में प्रत्येक Until घटक की यात्रा करती है।
4. सेफ्टी फिल्टरिंग: लेखक प्रदर्शित करते हैं कि Q-फंक्शन एक सुरक्षा फिल्टर के रूप में कार्य कर सकता है। वे एक विफलता सेट (failure set) को परिभाषित करते हैं जहाँ विनिर्देश को गैर-ऋणात्मक रोबस्टनेस के साथ संतुष्ट नहीं किया जा सकता है। एक न्यूनतम-प्रतिबंधात्मक हस्तक्षेप योजना (least-restrictive intervention scheme) प्रस्तावित है: यदि किसी नाममात्र (nominal) नीति का एक्शन एक गैर-ऋणात्मक Q-वैल्यू देता है (जो भविष्य की संतुष्टि का संकेत देता है), तो उसे अनुमति दी जाती है; अन्यथा, सिस्टम उस एक्शन पर स्विच करता है जो Q-फंक्शन को अधिकतम करता है। विशिष्ट धारणाओं (जैसे, अनबाउंडेड Until ऑपरेटर्स की अनुपस्थिति) के तहत, यह फिल्टर विनिर्देश संतुष्टि की गारंटी देता है।

मुख्य योगदान

1. वैल्यू फंक्शन्स का सामान्यीकरण: पेपर स्टेट हिस्ट्रीज़ (परिभाषा 1) पर इष्टतम वैल्यू फंक्शन और Q-फंक्शन को सामान्यीकृत करता है और हिस्टरीज पर ऑप्टिमलिटी को परिभाषित करता है (परिभाषा 2), जो अनंत-क्षितिज TL समस्याओं की नॉन-मार्कोवियन प्रकृति को संबोधित करता है।
2. कंपोजिशनल इष्टतम नीतियां: TL फॉर्मूला के एक व्यापक वर्ग (परिभाषा 3) के लिए, लेखक संबंधित रोबस्टनेस मेट्रिक के लिए कंपोजिशनल इष्टतम नीतियां निर्मित करते हैं (थ्योरम 1–8)। इसमें Until और Globally-Until विनिर्देशों में होने वाली टालने की पैथोलॉजी को संभालना शामिल है।
3. न्यूनतम-प्रतिबंधात्मक सुरक्षा फिल्टर: यह कार्य दिखाता है कि (संभावित रूप से उप-इष्टतम) हिस्टरीज पर Q-फंक्शन एक नाममात्र नीति के लिए एक न्यूनतम-प्रतिबंधात्मक सुरक्षा फिल्टर प्रदान करता है (थ्योरम 9, 10)। यह फिल्टर, बशर्ते कि फॉर्मूला कुछ संरचनात्मक बाधाओं को पूरा करता हो, नाममात्र नीति के पूर्व पथ का सम्मान करते हुए विनिर्देश संतुष्टि की गारंटी देता है।

परिणाम और प्रदर्शन
पेपर अपने प्रस्तावित ढांचे को सैद्धांतिक प्रमाणों और दो हार्डवेयर/सॉफ्टवेयर प्रदर्शनों के माध्यम से मान्य करता है:

• टू-एजेंट ग्रिडवर्ल्ड: लेखक एक जटिल विनिर्देश वाले 4-आयामी संयुक्त स्टेट-एक्शन समस्या को हल करते हैं जिसमें समय-बद्ध रीच, सुरक्षा और जीवंतता (liveness) संबंधी बाधाएं शामिल हैं। वे प्रदर्शित करते हैं कि व्युत्पन्न इष्टतम नीति ($\pi_{spec}$) सफलतापूर्वक सिस्टम को विनिर्देश को संतुष्ट करने के लिए निर्देशित करती है। इसके अतिरिक्त, जब इसे "कॉफी" और "टी" नाममात्र नीतियों के लिए एक फिल्टर के रूप में उपयोग किया जाता है (जो व्यक्तिगत रूप से संयुक्त विनिर्देश को संतुष्ट करने में विफल रहती हैं), तो यह फिल्टर सुनिश्चित करता है कि संयुक्त सिस्टम जटिल कार्य को संतुष्ट करता है, जबकि एक मानक "केवल-सुरक्षा" फिल्टर डेडलॉक और विफलता की ओर ले जाता है।
• सिंगल-एजेंट ड्रोन: एक क्रेजीफ्लाई (Crazyflie) ड्रोन का उपयोग करके, लेखक बाधाओं वाले नेविगेशन कार्य में इस नीति का प्रदर्शन करते हैं। प्रस्तावित TL फिल्टर ड्रोन को जटिल टेम्पोरल बाधाओं (जैसे, विशिष्ट ज़ोन में घूमना, दीवारों से बचना) को संतुष्ट करते हुए कार्यस्थल तक सफलतापूर्वक निर्देशित करता है। इसके विपरीत, एक अनफिल्टर्ड नाममात्र नीति या केवल सुरक्षा बाधाओं पर आधारित फिल्टर ड्रोन को फंसने या क्रैश होने का कारण बनता है।

महत्व
पेपर दावा करता है कि यह हालिया अपघटन परिणामों का विस्तार करके, एक विस्तृत वर्ग के TL फॉर्मूला के मूल्य के लिए इष्टतम नीतियां उत्पन्न करने के लिए एक व्यावहारिक दृष्टिकोण प्रदान करता है। इसका प्राथमिक महत्व इस पैथोलॉजी को हल करने में है जहाँ लालची Q-मैक्सिमाइजेशन अनंत-क्षितिज कार्यों के लिए विफल हो जाता है और जटिल कार्य संतुष्टि (केवल सुरक्षा नहीं) सुनिश्चित करने वाले सुरक्षा फिल्टरों के लिए एक तंत्र प्रदान करने में है। Until और Globally-Until विनिर्देशों को शामिल करने के लिए हल करने योग्य फॉर्मूला के दायरे को बढ़ाकर, यह कार्य जटिल, सुरक्षा-महत्वपूर्ण टेम्पोरल कार्यों के लिए हैमिल्टोन-जैकबी (Hamilton-Jacobi) रीचेबिलिटी और सुदृढीकरण लर्निंग (Reinforcement Learning) के बीच के अंतर को पाटता है।