Principles of Model Checking
मॉडल जाँच के सिद्धांत मॉडल जाँच पर एक पाठ्यपुस्तक है, जो कंप्यूटर विज्ञान का एक क्षेत्र है जो यह निर्धारित करने की समस्या को स्वचालित करता है कि क्या कोई मशीन विनिर्देशन आवश्यकताओं को पूरा करती है। यह क्रिस्टेल बेयर और जूस्ट-पीटर कैटोएन द्वारा लिखा गया था, और 2008 में एमआईटी प्रेस द्वारा प्रकाशित किया गया था। परिचय और पहला अध्याय मॉडल जाँच के क्षेत्र की रूपरेखा तैयार करता हैः एक मशीन या प्रक्रिया के एक मॉडल का विश्लेषण यह देखने के लिए किया जा सकता है कि क्या वांछनीय गुण हैं। उदाहरण के लिए, एक वेंडिंग मशीन इस संपत्ति को संतुष्ट कर सकती है कि "शेष राशि कभी भी 0,00 यूरो से नीचे नहीं गिर सकती है।" एक वीडियो गेम इस नियम को लागू कर सकता है "यदि खिलाड़ी के पास 0 जीवन है तो खेल नुकसान में समाप्त होता है"। वेंडिंग मशीन और वीडियो गेम दोनों को संक्रमण प्रणाली के रूप में मॉडल किया जा सकता है। मॉडल जाँच गणितीय भाषा में ऐसी आवश्यकताओं का वर्णन करने की प्रक्रिया है, और प्रमाणों को स्वचालित करना है कि मॉडल आवश्यकताओं को पूरा करता है, या यदि मॉडल दोषपूर्ण है तो प्रति-उदाहरणों की खोज। दूसरा अध्याय समवर्ती प्रणालियों के लिए एक उपयुक्त मॉडल बनाने पर केंद्रित है, जहां एक एल्गोरिथ्म के कई भागों (निर्देशों का सेट) को विभिन्न मशीनों या मशीन के हिस्सों द्वारा एक साथ किया जा सकता है। अध्याय 3 उन नियमों के प्रकारों की खोज करता है जिन्हें एक संक्रमण प्रणाली संतुष्ट कर सकती हैः रैखिक समय गुण। एक सुरक्षा गुण, जैसे कि "कोई गतिरोध स्थिति संभव नहीं है", इस रूप का है कि "एक अवांछनीय परिणाम कभी नहीं हो सकता है"। एक जीवंत संपत्ति, जैसे कि "एक साझा संसाधन हमेशा अंततः एक घटक के लिए उपलब्ध कराया जाएगा जो इसका अनुरोध करता है", इस रूप में है "एक वांछनीय परिणाम अंततः होगा"। निष्पक्षता गुण जैसे "ट्रैफिक लाइट कभी भी रंग बदलना बंद नहीं करती" का उपयोग पूर्व शर्तों के रूप में किया जा सकता है। ऐसी धारणाएँ जिनसे अन्य गुणों का अनुमान लगाया जा सकता है। चौथा अध्याय नियमित और ω-नियमित भाषा गुणों और बुची ऑटोमेटा जैसी सैद्धांतिक मशीनों के बारे में है जो भाषाओं का मॉडल बनाते हैं। यह गुणों को सत्यापित करने या प्रति-उदाहरण खोजने के लिए मॉडल-जाँच एल्गोरिदम देता है। पाँचवाँ और छठा अध्याय रैखिक लौकिक तर्क (एल. टी. एल.) और गणना वृक्ष तर्क (सी. टी. एल.) का पता लगाते हैं, जो सूत्र के दो वर्ग हैं जो गुणों को व्यक्त करते हैं। एल. टी. एल. एक प्रणाली के माध्यम से पथ के बारे में आवश्यकताओं को कूटबद्ध करता है, जैसे कि "प्रत्येक एकाधिकार खिलाड़ी 'जाओ' को असीम रूप से बार-बार पारित करता है"; सी. टी. एल. एक प्रणाली में राज्यों के बारे में आवश्यकताओं को कूटबद्ध करता है, जैसे कि "किसी भी स्थिति से, सभी खिलाड़ी अंततः 'जाओ' पर उतर सकते हैं। सीटीएल * सूत्र, जो दो व्याकरणों को जोड़ते हैं, को भी परिभाषित किया गया है। इन तर्कों में मॉडल-जाँच सूत्र के लिए एल्गोरिदम दिए गए हैं। सातवाँ अध्याय संक्रमण प्रणालियों की तुलना करने के औपचारिक तरीकों की खोज करता है, जैसे कि द्विभाजन; आठवाँ आंशिक क्रम में कमी के बारे में है जिसका उद्देश्य एक मॉडल के गुणों को सत्यापित करने के लिए आवश्यक गणना को कम करना है। नौवें और दसवें अध्याय पहले विचार किए गए तर्क और स्वचालित के विस्तार के बारे में हैं, जिसमें घड़ी की गति (समयबद्ध स्वचालित) या संभावनाओं (मार्कोव श्रृंखलाओं पर आधारित संभावित स्वचालित) को जोड़ना शामिल है। रिसेप्शन फ्रैंकोइस लारोसीनी ने द कंप्यूटर जर्नल में लिखते हुए, पुस्तक को "प्रभावशाली" बताते हुए शोधकर्ताओं, व्याख्याताओं, छात्रों और इंजीनियरों को पुस्तक की सिफारिश की। लारौसिनी ने पाया कि पाठ्यपुस्तक व्यापक और सुलभ रूप से लिखी गई है, जिसमें अच्छी संख्या में उदाहरण, अभ्यास और प्रमुख अवधारणाओं के लिए प्रेरक विचार हैं। "एकीकृत ढांचे" के साथ, पहले सात अध्याय शास्त्रीय सिद्धांत को शामिल करते हैं और अंतिम तीन अध्याय मॉडल जाँच के विस्तार को शामिल करते हैं। एसीएम कम्प्यूटिंग रिव्यूज में, गैब्रियल सिओबानू का मानना था कि इस पाठ्यपुस्तक का उपयोग उन्नत स्नातक या स्नातक पाठ्यक्रमों में किया जा सकता है, और यह शोधकर्ताओं के लिए उपयोगी होगी। सिओबानू ने "स्पष्ट और सहज ज्ञान युक्त" प्रस्तुति की प्रशंसा की और कहा कि "मॉडल जाँच अनुसंधान में बुनियादी अवधारणाओं, गहन सैद्धांतिक परिणामों और उन्नत विषयों को शामिल करने के लिए इसके शैक्षणिक दृष्टिकोण की सराहना की जानी चाहिए।" 2014 में, यह पुस्तक बुक साइटेशन इंडेक्स (बी. के. सी. आई.) द्वारा निगरानी किए गए पांच सबसे अधिक उद्धृत शैक्षणिक ग्रंथों में से एक थी। संदर्भ आगे पढ़ने के लिए बाहरी लिंक आधिकारिक वेबसाइट 2008 गैर-काल्पनिक पुस्तकें कंप्यूटर विज्ञान की पाठ्यपुस्तकें