Principles of Model Checking
மாதிரி சரிபார்ப்பின் கோட்பாடுகள் என்பது மாதிரி சரிபார்ப்பு பற்றிய ஒரு பாடப்புத்தகமாகும், இது கணினி அறிவியலின் ஒரு பகுதியாகும், இது ஒரு இயந்திரம் விவரக்குறிப்பு தேவைகளைப் பூர்த்தி செய்கிறதா என்பதைத் தீர்மானிப்பதில் உள்ள சிக்கலை தானியக்கமாக்குகிறது. இது கிறிஸ்டல் பேயர் மற்றும் ஜூஸ்ட்-பீட்டர் கட்டோன் ஆகியோரால் எழுதப்பட்டு, 2008 ஆம் ஆண்டில் எம்ஐடி பிரஸ்ஸால் வெளியிடப்பட்டது. கதை சுருக்கம்ஃ அறிமுகமும் முதல் அத்தியாயமும் மாதிரி சரிபார்ப்பு துறையை கோடிட்டுக் காட்டுகின்றனஃ ஒரு இயந்திரம் அல்லது செயல்முறையின் மாதிரியை விரும்பத்தக்க பண்புகள் உள்ளனவா என்பதைப் பார்க்க பகுப்பாய்வு செய்யலாம். உதாரணமாக, ஒரு விற்பனை இயந்திரம் "இருப்பு ஒருபோதும் 0,00 யூரோக்களுக்கு கீழே வர முடியாது" என்ற சொத்தை திருப்திப்படுத்தலாம். ஒரு வீடியோ கேம் "வீரருக்கு 0 உயிர்கள் இருந்தால், விளையாட்டு இழப்பில் முடிவடைகிறது" என்ற விதியை அமல்படுத்தலாம். விற்பனை இயந்திரம் மற்றும் வீடியோ கேம் இரண்டையும் மாற்றம் அமைப்புகளாக வடிவமைக்க முடியும். மாதிரி சரிபார்ப்பு என்பது அத்தகைய தேவைகளை கணித மொழியில் விவரிக்கும் செயல்முறையாகும், மேலும் மாதிரி தேவைகளை பூர்த்தி செய்கிறது என்பதற்கான ஆதாரங்களை தானியக்கமாக்குகிறது, அல்லது மாதிரி தவறாக இருந்தால் எதிர் உதாரணங்களைக் கண்டுபிடிப்பது. இரண்டாவது அத்தியாயம் ஒருங்கிணைந்த அமைப்புகளுக்கு பொருத்தமான மாதிரியை உருவாக்குவதில் கவனம் செலுத்துகிறது, அங்கு ஒரு வழிமுறையின் பல பகுதிகளை (அறிவுறுத்தல்களின் தொகுப்பு) ஒரே நேரத்தில் வெவ்வேறு இயந்திரங்கள் அல்லது ஒரு இயந்திரத்தின் பகுதிகளால் மேற்கொள்ள முடியும். அத்தியாயங்கள் 3 ஒரு இடைநிலை அமைப்பு பூர்த்தி செய்யக்கூடிய விதிகளின் வகைகளை ஆராய்கிறதுஃ நேரியல் நேர பண்புகள். "முட்டுக்கட்டை நிலைகள் சாத்தியமில்லை" போன்ற ஒரு பாதுகாப்பு பண்பு, "விரும்பத்தகாத விளைவு ஒருபோதும் ஏற்படாது" என்ற வடிவத்தில் உள்ளது. "ஒரு பகிரப்பட்ட வளம் எப்போதும் அதைக் கோரும் ஒரு கூறுக்கு இறுதியில் கிடைக்கும்" போன்ற ஒரு உயிர்ச்சக்தி பண்பு, "விரும்பத்தக்க முடிவு இறுதியில் நடக்கும்" என்ற வடிவத்தில் உள்ளது. "போக்குவரத்து விளக்கு நிறத்தை மாற்றுவதை ஒருபோதும் நிறுத்தாது" போன்ற நியாயமான பண்புகள் முன்நிபந்தனைகளாக பயன்படுத்தப்படலாம், அதாவது. பிற பண்புகளை யூகிக்கக்கூடிய அனுமானங்கள். நான்காவது அத்தியாயம் வழக்கமான மற்றும் ω-வழக்கமான மொழி பண்புகள் மற்றும் மொழிகளை மாதிரியாகக் கொண்ட புச்சி ஆட்டோமேட்டா போன்ற கோட்பாட்டு இயந்திரங்களைப் பற்றியது. இது பண்புகளை சரிபார்க்க அல்லது எதிர் உதாரணங்களைக் கண்டறிய மாதிரி-சரிபார்ப்பு வழிமுறைகளை வழங்குகிறது. ஐந்தாவது மற்றும் ஆறாவது அத்தியாயங்கள் நேரியல் தற்காலிக தர்க்கம் (எல். டி. எல்) மற்றும் கணக்கீட்டு மர தர்க்கம் (சி. டி. எல்), பண்புகளை வெளிப்படுத்தும் இரண்டு வகை சூத்திரங்களை ஆராய்கின்றன. எல். டி. எல் ஒரு அமைப்பின் வழியாக பாதைகளைப் பற்றிய தேவைகளை குறியாக்கம் செய்கிறது, அதாவது "ஒவ்வொரு ஏகபோக வீரரும் 'கோ' ஐ எல்லையற்ற அடிக்கடி கடந்து செல்கிறார்"; சி. டி. எல் ஒரு அமைப்பில் உள்ள நிலைகளைப் பற்றிய தேவைகளை குறியாக்கம் செய்கிறது, அதாவது "எந்த நிலையிலிருந்தும், அனைத்து வீரர்களும் இறுதியில் 'கோ' இல் தரையிறங்க முடியும்". இரண்டு இலக்கணங்களையும் இணைக்கும் சி. டி. எல் * சூத்திரங்களும் வரையறுக்கப்படுகின்றன. இந்த தர்க்கங்களில் மாதிரி-சரிபார்ப்பு சூத்திரங்களுக்கான வழிமுறைகள் கொடுக்கப்பட்டுள்ளன. ஏழாவது அத்தியாயம் இருதரப்பு உருவகப்படுத்துதல் போன்ற மாற்றம் அமைப்புகளை ஒப்பிடுவதற்கான முறையான வழிகளை ஆராய்கிறது; எட்டாவது ஒரு மாதிரியின் பண்புகளை சரிபார்க்க தேவையான கணக்கீட்டைக் குறைப்பதை நோக்கமாகக் கொண்ட பகுதி வரிசைக் குறைப்புகளைப் பற்றியது. ஒன்பதாவது மற்றும் பத்தாவது அத்தியாயங்கள் முன்பு கருதப்பட்ட தர்க்கவியல் மற்றும் தானியங்கி விரிவாக்கங்களைப் பற்றியது, இதில் கடிகார வேகம் (நேர தானியங்கி) அல்லது நிகழ்தகவுகள் (மார்கோவ் சங்கிலிகளை அடிப்படையாகக் கொண்ட நிகழ்தகவு தானியங்கி) ஆகியவை அடங்கும். தி கம்ப்யூட்டர் ஜர்னலில் எழுதிய வரவேற்பு பிரான்சுவா லாரோசினி, ஆராய்ச்சியாளர்கள், விரிவுரையாளர்கள், மாணவர்கள் மற்றும் பொறியாளர்களுக்கு இந்த புத்தகத்தை பரிந்துரைத்தார், இந்த புத்தகத்தை "ஈர்க்கக்கூடியது" என்று அழைத்தார். ஏராளமான எடுத்துக்காட்டுகள், பயிற்சிகள் மற்றும் முக்கிய கருத்துக்களுக்கான ஊக்கமளிக்கும் யோசனைகளுடன் விரிவான மற்றும் அணுகக்கூடிய வகையில் எழுதப்பட்ட பாடப்புத்தகத்தை லாரோசினி கண்டறிந்தார். ஒரு "ஒருங்கிணைந்த கட்டமைப்புடன்", முதல் ஏழு அத்தியாயங்கள் பாரம்பரிய கோட்பாட்டை உள்ளடக்கியது மற்றும் கடைசி மூன்று அத்தியாயங்கள் மாதிரி சரிபார்ப்பின் விரிவாக்கங்களை உள்ளடக்கியது. ஏ. சி. எம் கம்ப்யூட்டிங் விமர்சனங்களில், கேப்ரியல் சியோபானு இந்த பாடப்புத்தகத்தை மேம்பட்ட இளங்கலை அல்லது பட்டதாரி படிப்புகளில் பயன்படுத்தலாம் என்றும் ஆராய்ச்சியாளர்களுக்கு பயனுள்ளதாக இருக்கும் என்றும் நம்பினார். சியோபானு "தெளிவான மற்றும் உள்ளுணர்வு" விளக்கக்காட்சியைப் பாராட்டினார், மேலும் இது "அடிப்படை கருத்துக்கள், ஆழமான தத்துவார்த்த முடிவுகள் மற்றும் மாதிரி சோதனை ஆராய்ச்சியில் மேம்பட்ட தலைப்புகளை உள்ளடக்கிய அதன் கற்பித்தல் அணுகுமுறைக்காக பாராட்டப்பட வேண்டும்" என்றார். 2014 ஆம் ஆண்டில், புத்தக மேற்கோள் குறியீட்டால் (பி. கே. சி. ஐ) கண்காணிக்கப்பட்ட ஐந்து மிகவும் மேற்கோள் காட்டப்பட்ட கல்வி நூல்களில் இதுவும் ஒன்றாகும். குறிப்புகள் மேலும் வாசிப்பு வெளிப்புற இணைப்புகள் அதிகாரப்பூர்வ வலைத்தளம் 2008 புனைகதை அல்லாத புத்தகங்கள் கணினி அறிவியல் பாடப்புத்தகங்கள்