Kripke structure (model checking)
यह लेख क्रिप्के संरचनाओं का वर्णन करता है जैसा कि मॉडल जाँच में उपयोग किया जाता है। अधिक सामान्य विवरण के लिए, क्रिप्के शब्दार्थ देखें। क्रिप्के संरचना संक्रमण प्रणाली की एक भिन्नता है, जिसे मूल रूप से शाऊल क्रिप्के द्वारा प्रस्तावित किया गया था, जिसका उपयोग किसी प्रणाली के व्यवहार का प्रतिनिधित्व करने के लिए मॉडल जाँच में किया जाता है। इसमें एक ग्राफ होता है जिसके नोड्स सिस्टम की पहुंच योग्य स्थितियों का प्रतिनिधित्व करते हैं और जिनके किनारे स्थिति संक्रमण का प्रतिनिधित्व करते हैं, एक लेबलिंग फ़ंक्शन के साथ जो प्रत्येक नोड को गुणों के एक समूह में मैप करता है जो संबंधित स्थिति में होता है। अस्थायी तर्कों की पारंपरिक रूप से क्रिप्के संरचनाओं के संदर्भ में व्याख्या की जाती है। औपचारिक परिभाषा आइए परमाणु प्रस्तावों का एक समूह हों, अर्थात। चर, स्थिरांक और विधेय प्रतीकों से बनी बूलियन-मूल्यवान अभिव्यक्तियाँ। क्लार्क एट अल। क्रिप्के संरचना को 4-टुपल के रूप में परिभाषित करें जिसमें अवस्थाओं का एक सीमित समूह होता है। प्रारंभिक अवस्थाओं का एक समूह। एक संक्रमण संबंध जो कि लेफ्ट-टोटल है, अर्थात, ऐसा है। एक लेबलिंग (या व्याख्या) कार्य। चूंकि कुल बचा हुआ है, इसलिए क्रिप्के संरचना के माध्यम से एक अनंत मार्ग का निर्माण करना हमेशा संभव है। एक गतिरोध स्थिति को एक एकल बहिर्गामी किनारे द्वारा मॉडल किया जा सकता है। लेबलिंग फ़ंक्शन प्रत्येक अवस्था के लिए सभी परमाणु प्रस्तावों के सेट को परिभाषित करता है जो मान्य हैं। संरचना का एक पथ अवस्थाओं का एक क्रम है जो प्रत्येक के लिए धारण करता है। पथ पर शब्द परमाणु प्रस्तावों के समुच्चय का अनुक्रम है, जो वर्णमाला पर एक ω-शब्द है। इस परिभाषा के साथ, एक क्रिप्के संरचना (मान लीजिए, केवल एक प्रारंभिक अवस्था वाली) को एक सिंगलटन इनपुट वर्णमाला के साथ एक मूर मशीन के साथ पहचाना जा सकता है, और आउटपुट फ़ंक्शन इसके लेबलिंग फ़ंक्शन के साथ। उदाहरण परमाणु प्रस्तावों के समूह को लें। और उस प्रणाली के मनमाने बूलियन गुणों को मॉडल कर सकते हैं जिसे क्रिप्के संरचना मॉडलिंग कर रही है। दाहिनी ओर का चित्र एक क्रिप्के संरचना को दर्शाता है, जहाँ। .. .. .. एक पथ उत्पन्न कर सकता है और पथ पर निष्पादन शब्द है। भाषा से संबंधित निष्पादन शब्दों का उत्पादन कर सकते हैं। यद्यपि यह शब्दावली मॉडल जाँच समुदाय में व्यापक है, मॉडल जाँच पर कुछ पाठ्यपुस्तकें इस विस्तारित तरीके से (या वास्तव में बिल्कुल भी) "क्रिप्के संरचना" को परिभाषित नहीं करती हैं, लेकिन केवल एक (लेबल) संक्रमण प्रणाली की अवधारणा का उपयोग करती हैं, जिसमें अतिरिक्त रूप से कार्यों का एक समूह होता है, और संक्रमण संबंध को एक उपसमुच्चय के रूप में परिभाषित किया जाता है, जिसे वे अतिरिक्त रूप से परमाणु प्रस्तावों के एक समूह और राज्यों के लिए एक लेबलिंग फ़ंक्शन को भी शामिल करने के लिए विस्तारित करते हैं (जैसा कि ऊपर परिभाषित किया गया है)। इस दृष्टिकोण में, क्रिया लेबल को हटा कर प्राप्त द्विआधारी संबंध को अवस्था ग्राफ कहा जाता है। क्लार्क एट अल। क्रिप्के संरचना को परिवर्तनों के एक समूह के रूप में पुनर्परिभाषित करें (केवल एक के बजाय), जो ऊपर दिए गए लेबल किए गए परिवर्तनों के बराबर है, जब वे मोडल μ-कैलकुलस के शब्दार्थ को परिभाषित करते हैं। यह भी देखें कि क्रिप्के शब्दार्थ की जाँच करने वाला अस्थायी तर्क मॉडल रैखिक अस्थायी तर्क गणना वृक्ष तर्क संदर्भ मॉडल अस्थायी तर्क संक्रमण प्रणालियों की जाँच कर रहा है।