Well-structured transition system
कंप्यूटर विज्ञान में, विशेष रूप से औपचारिक सत्यापन के क्षेत्र में, अच्छी तरह से संरचित संक्रमण प्रणाली (डब्ल्यू. एस. टी. एस.) अनंत अवस्था प्रणालियों का एक सामान्य वर्ग है जिसके लिए कई सत्यापन समस्याएं निर्णायक हैं, जो प्रणाली की स्थितियों के बीच एक प्रकार के क्रम के अस्तित्व के कारण है जो प्रणाली के संक्रमण के साथ संगत है। डब्ल्यू. एस. टी. एस. निर्णायकता परिणामों को पेट्री नेट, हानिपूर्ण चैनल सिस्टम और बहुत कुछ पर लागू किया जा सकता है। औपचारिक परिभाषा याद रखें कि एक सेट पर एक अच्छी तरह से अर्ध-आदेश एक अर्ध-आदेश (यानी, एक पूर्व क्रम या प्रतिवर्तक, सकर्मक द्विआधारी संबंध) है जैसे कि तत्वों के किसी भी अनंत अनुक्रम में, के साथ एक बढ़ती जोड़ी होती है। कहा जाता है कि सेट अच्छी तरह से अर्ध-आदेशित है, या जल्द ही डब्ल्यूक्यूओ। हमारे उद्देश्यों के लिए, एक संक्रमण प्रणाली एक संरचना है, जहाँ कोई भी समूह (इसके तत्वों को अवस्थाएँ कहा जाता है), और (इसके तत्वों को संक्रमण कहा जाता है)। सामान्य तौर पर एक संक्रमण प्रणाली में अतिरिक्त संरचना हो सकती है जैसे प्रारंभिक अवस्थाएँ, संक्रमण पर लेबल, अवस्थाओं को स्वीकार करना आदि। (बिंदुओं द्वारा इंगित), लेकिन वे यहाँ हमें चिंतित नहीं करते हैं। एक अच्छी तरह से संरचित संक्रमण प्रणाली में एक संक्रमण प्रणाली होती है, जो अवस्थाओं के समूह पर एक अच्छी तरह से अर्ध-आदेश है। ऊपर की ओर संगत हैः अर्थात, सभी संक्रमणों के लिए (इससे हमारा मतलब है) और ऐसे सभी के लिए, ऐसा मौजूद है कि (यानी, शून्य या अधिक संक्रमणों के अनुक्रम से पहुँचा जा सकता है) और। एक अच्छी तरह से संरचित प्रणाली एक संक्रमण प्रणाली है जिसमें एक सीमित नियंत्रण स्थिति सेट से बना राज्य सेट होता है, एक डेटा मूल्य सेट, एक निर्णायक पूर्व-क्रम के साथ सुसज्जित होता है जिसे राज्यों तक विस्तारित किया जाता है, जो ऊपर परिभाषित के रूप में अच्छी तरह से संरचित होता है (मोनोटोनिक है, अर्थात। ऊपर की ओर संगत, के संबंध में) और इसके अलावा किसी भी ऊपर की ओर बंद सबसेट के पूर्ववर्तियों के सेट के लिए मिनीमा का एक कम्प्यूटेबल सेट है। अच्छी तरह से संरचित प्रणालियाँ कंप्यूटर विज्ञान में सामना की जाने वाली प्रणालियों के कुछ वर्गों के मॉडलिंग के लिए अच्छी तरह से संरचित संक्रमण प्रणालियों के सिद्धांत को अनुकूलित करती हैं और ऐसी प्रणालियों का विश्लेषण करने के लिए निर्णय प्रक्रियाओं के लिए आधार प्रदान करती हैं, इसलिए पूरक आवश्यकताएँः डब्ल्यू. एस. टी. एस. की परिभाषा स्वयं संबंधों की संगणनाशीलता के बारे में कुछ नहीं कहती है। कंप्यूटर विज्ञान में उपयोग अच्छी तरह से संरचित प्रणालियों की व्याप्ति को किसी भी अच्छी तरह से संरचित प्रणाली के लिए तय किया जा सकता है, और इसलिए अब्दुल्ला एट अल के पिछड़े एल्गोरिदम द्वारा किसी दिए गए नियंत्रण स्थिति की पहुंच निर्धारित की जा सकती है। या अच्छी तरह से संरचित प्रणालियों के विशिष्ट उपवर्गों के लिए (सख्त एकरसता के अधीन, जैसे। सीमाहीन पेट्री जाल के मामले में) एक कार्प-मिलर आच्छादन ग्राफ के आधार पर एक आगे के विश्लेषण द्वारा। बैकवर्ड एल्गोरिदम बैकवर्ड एल्गोरिदम निम्नलिखित प्रश्न का उत्तर देने की अनुमति देता हैः एक अच्छी तरह से संरचित प्रणाली और एक अवस्था को देखते हुए, क्या कोई संक्रमण मार्ग है जो किसी दिए गए प्रारंभिक अवस्था से किसी अवस्था की ओर ले जाता है (ऐसी अवस्था को कवर कहा जाता है)? इस प्रश्न के लिए एक सहज स्पष्टीकरण हैः यदि एक त्रुटि स्थिति का प्रतिनिधित्व करता है, तो इसे रखने वाली किसी भी स्थिति को भी एक त्रुटि स्थिति के रूप में माना जाना चाहिए। यदि एक अच्छी तरह से अर्ध-क्रम पाया जा सकता है जो राज्यों के इस "नियंत्रण" को मॉडल करता है और जो संक्रमण संबंध के संबंध में एकरसता की आवश्यकता को भी पूरा करता है, तो इस प्रश्न का उत्तर दिया जा सकता है। एक न्यूनतम त्रुटि अवस्था के बजाय, आमतौर पर त्रुटि अवस्थाओं के एक ऊपर की ओर बंद समूह पर विचार किया जाता है। एल्गोरिथ्म इन तथ्यों पर आधारित है कि एक अच्छी तरह से अर्ध-क्रम में, किसी भी ऊपर की ओर बंद सेट में मिनीमा का एक सीमित सेट होता है, और ऊपर की ओर बंद उपसमुच्चय का कोई भी अनुक्रम सीमित रूप से कई चरणों (1) के बाद अभिसरण करता है। एल्गोरिथम को मेमोरी में अवस्थाओं के एक ऊपर की ओर बंद सेट को संग्रहीत करने की आवश्यकता होती है, जो यह कर सकता है क्योंकि एक ऊपर की ओर बंद सेट को मिनीमा के एक सीमित सेट के रूप में दर्शाया जा सकता है। यह त्रुटि अवस्थाओं के सेट के ऊपर की ओर बंद होने से शुरू होता है और प्रत्येक पुनरावृत्ति पर तत्काल पूर्ववर्तियों के सेट (एकरसता द्वारा भी ऊपर की ओर बंद) की गणना करता है और इसे सेट में जोड़ता है। यह पुनरावृत्ति अच्छी तरह से अर्ध-आदेशों के गुण (1) के कारण सीमित संख्या में चरणों के बाद समाप्त हो जाती है। यदि अंत में प्राप्त सेट में है, तो आउटपुट "हाँ" है (एक स्थिति तक पहुँचा जा सकता है), अन्यथा यह "नहीं" है (ऐसी स्थिति तक पहुँचना संभव नहीं है)। संदर्भ अच्छी तरह से स्थापित स्वचालन (गणना)