Partial order reduction
कंप्यूटर विज्ञान में, आंशिक क्रम में कमी एक मॉडल चेकिंग या स्वचालित योजना और शेड्यूलिंग एल्गोरिदम द्वारा खोजे जाने वाले राज्य-स्थान के आकार को कम करने की एक तकनीक है। यह समवर्ती रूप से निष्पादित संक्रमणों की कम्यूटेटिविटी का फायदा उठाता है जिसके परिणामस्वरूप अलग-अलग क्रम में निष्पादित होने पर एक ही स्थिति होती है। स्पष्ट अवस्था अंतरिक्ष अन्वेषण में, आंशिक क्रम में कमी आमतौर पर सभी सक्षम संक्रमणों के प्रतिनिधि उपसमुच्चय के विस्तार की विशिष्ट तकनीक को संदर्भित करती है। इस तकनीक को प्रतिनिधियों के साथ मॉडल जाँच के रूप में भी वर्णित किया गया है। विधि के विभिन्न संस्करण हैं, तथाकथित जिद्दी सेट विधि, पर्याप्त सेट विधि और लगातार सेट विधि। एम्पल सेट प्रतिनिधियों के साथ मॉडल की जाँच का एक उदाहरण है। उनका सूत्रीकरण निर्भरता की एक अलग धारणा पर निर्भर करता है। दो संक्रमणों को केवल तभी स्वतंत्र माना जाता है जब वे पारस्परिक रूप से सक्षम होने पर दूसरे को अक्षम नहीं कर सकते हैं। जिस क्रम में उन्हें निष्पादित किया जाता है, उस पर ध्यान दिए बिना दोनों का निष्पादन एक अद्वितीय स्थिति में होता है। जो परिवर्तन स्वतंत्र नहीं हैं, वे निर्भर हैं। व्यवहार में निर्भरता को स्थिर विश्लेषण का उपयोग करके अनुमानित किया जाता है। विभिन्न उद्देश्यों के लिए विशाल समुच्चय को इस शर्त के साथ परिभाषित किया जा सकता है कि किसी दिए गए राज्य में परिवर्तनों का एक समुच्चय कब "पर्याप्त" है। सी0 सी1 यदि एक संक्रमण कुछ संक्रमण संबंध पर निर्भर करता है, तो इस संक्रमण को तब तक लागू नहीं किया जा सकता जब तक कि पर्याप्त सेट में कुछ संक्रमण निष्पादित नहीं किया जाता है। सी0 और सी1 स्थितियाँ राज्य क्षेत्र में सभी गतिरोधों को संरक्षित करने के लिए पर्याप्त हैं। अधिक सूक्ष्म गुणों को संरक्षित करने के लिए और प्रतिबंधों की आवश्यकता है। उदाहरण के लिए, रैखिक लौकिक तर्क के गुणों को संरक्षित करने के लिए, निम्नलिखित दो शर्तों की आवश्यकता होती हैः C2 यदि, पर्याप्त समुच्चय में प्रत्येक संक्रमण अदृश्य है। सी 3 ए चक्र की अनुमति नहीं है यदि इसमें एक ऐसी स्थिति है जिसमें कुछ संक्रमण सक्षम है, लेकिन चक्र पर किसी भी अवस्था के लिए पर्याप्त (ओं) में कभी भी शामिल नहीं है। ये स्थितियाँ एक पर्याप्त समूह के लिए पर्याप्त हैं, लेकिन आवश्यक स्थितियों के लिए पर्याप्त नहीं हैं। जिद्दी सेट जिद्दी सेट एक स्पष्ट स्वतंत्रता संबंध का कोई उपयोग नहीं करते हैं। इसके बजाय उन्हें केवल क्रियाओं के अनुक्रमों पर कम्यूटेटिविटी के माध्यम से परिभाषित किया जाता है। एक सेट s पर (कमजोर रूप से) जिद्दी होता है, यदि निम्नलिखित पकड़। D0, यदि अनुक्रम का निष्पादन संभव है और अवस्था की ओर ले जाता है, तो अनुक्रम का निष्पादन संभव है और अवस्था की ओर ले जाएगा। डी1 या तो एक गतिरोध है, या ऐसा है कि इसका निष्पादन संभव है। ये स्थितियाँ सभी गतिरोधों को संरक्षित करने के लिए पर्याप्त हैं, जैसे सी0 और सी1 पर्याप्त निर्धारित विधि में हैं। हालाँकि, वे कुछ हद तक कमजोर हैं, और इस तरह से छोटे समूह हो सकते हैं। सी2 और सी3 स्थितियों को पर्याप्त सेट विधि से और कमजोर किया जा सकता है, लेकिन जिद्दी सेट विधि सी2 और सी3 के साथ संगत है। अन्य आंशिक क्रम में कमी के लिए अन्य संकेतन भी हैं। आमतौर पर उपयोग किए जाने वाले एल्गोरिदम में से एक स्थायी सेट/स्लीप सेट एल्गोरिदम है। पैट्रिस गोडफ्रॉइड के शोध प्रबंध में विस्तृत जानकारी मिल सकती है। प्रतीकात्मक मॉडल जाँच में, अधिक बाधाओं (गार्ड सुदृढ़ीकरण) को जोड़कर आंशिक क्रम में कमी हासिल की जा सकती है। आंशिक क्रम में कमी के आगे के अनुप्रयोगों में स्वचालित योजना शामिल है। उद्धरण संदर्भ मॉडल जाँच