Principles of Model Checking
মডেল চেকিংয়ের নীতিগুলি হল মডেল চেকিংয়ের উপর একটি পাঠ্যপুস্তক, যা কম্পিউটার বিজ্ঞানের একটি ক্ষেত্র যা একটি যন্ত্র নির্দিষ্টকরণের প্রয়োজনীয়তা পূরণ করে কিনা তা নির্ধারণের সমস্যাটিকে স্বয়ংক্রিয় করে। এটি ক্রিস্টেল বায়ার এবং জুস্ট-পিটার কাটোয়েন লিখেছেন এবং 2008 সালে এমআইটি প্রেস দ্বারা প্রকাশিত হয়েছিল। ভূমিকা এবং প্রথম অধ্যায় মডেল চেকিংয়ের ক্ষেত্রের রূপরেখা দেয়ঃ একটি মেশিন বা প্রক্রিয়ার একটি মডেল বিশ্লেষণ করে দেখা যেতে পারে যে পছন্দসই বৈশিষ্ট্যগুলি ধারণ করে কিনা। উদাহরণস্বরূপ, একটি ভেন্ডিং মেশিন এই বৈশিষ্ট্যটি সন্তুষ্ট করতে পারে যে "ব্যালেন্স কখনই 0,00 ইউরোর নিচে নামতে পারে না"। একটি ভিডিও গেম এই নিয়মটি প্রয়োগ করতে পারে "যদি খেলোয়াড়ের 0 জীবন থাকে তবে খেলাটি লোকসানে শেষ হয়"। ভেন্ডিং মেশিন এবং ভিডিও গেম উভয়ই ট্রানজিশন সিস্টেম হিসাবে মডেল করা যেতে পারে। মডেল চেকিং হল গাণিতিক ভাষায় এই ধরনের প্রয়োজনীয়তাগুলি বর্ণনা করার প্রক্রিয়া, এবং স্বয়ংক্রিয় প্রমাণ যে মডেলটি প্রয়োজনীয়তাগুলি পূরণ করে, বা মডেলটি ত্রুটিপূর্ণ হলে পাল্টা উদাহরণগুলির আবিষ্কার। দ্বিতীয় অধ্যায়টি সমবর্তী ব্যবস্থার জন্য একটি উপযুক্ত মডেল তৈরি করার উপর দৃষ্টি নিবদ্ধ করে, যেখানে একটি অ্যালগরিদমের একাধিক অংশ (নির্দেশাবলীর সেট) বিভিন্ন মেশিন বা একটি মেশিনের অংশ দ্বারা একযোগে পরিচালিত হতে পারে। অধ্যায় 3 এমন ধরনের নিয়মের অন্বেষণ করে যা একটি রূপান্তর ব্যবস্থা সন্তুষ্ট করতে পারেঃ রৈখিক সময়ের বৈশিষ্ট্য। একটি নিরাপত্তা বৈশিষ্ট্য, যেমন "কোনও অচল অবস্থা সম্ভব নয়", "একটি অবাঞ্ছিত ফলাফল কখনই ঘটতে পারে না"। একটি প্রাণবন্ত সম্পত্তি, যেমন "একটি ভাগ করা সম্পদ সর্বদা শেষ পর্যন্ত এমন একটি উপাদানের জন্য উপলব্ধ করা হবে যা এটি অনুরোধ করে", "একটি কাঙ্ক্ষিত ফলাফল অবশেষে ঘটবে"। "ট্রাফিক লাইট কখনই রঙ পরিবর্তন করা বন্ধ করে না"-এর মতো ন্যায্য বৈশিষ্ট্যগুলি পূর্বশর্ত হিসাবে ব্যবহার করা যেতে পারে। অনুমান যা থেকে অন্যান্য বৈশিষ্ট্য অনুমান করা যেতে পারে। চতুর্থ অধ্যায়টি নিয়মিত এবং ω-নিয়মিত ভাষার বৈশিষ্ট্য এবং বুচি অটোমাটার মতো তাত্ত্বিক যন্ত্র সম্পর্কে যা ভাষাগুলির মডেল তৈরি করে। এটি বৈশিষ্ট্যগুলি যাচাই করতে বা পাল্টা উদাহরণগুলি খুঁজে পেতে মডেল-চেকিং অ্যালগরিদম দেয়। পঞ্চম এবং ষষ্ঠ অধ্যায়গুলি রৈখিক সাময়িক যুক্তি (এল. টি. এল) এবং গণনা বৃক্ষ যুক্তি (সি. টি. এল), দুটি শ্রেণীর সূত্র যা বৈশিষ্ট্য প্রকাশ করে তা অন্বেষণ করে। এলটিএল একটি সিস্টেমের মাধ্যমে পথ সম্পর্কে প্রয়োজনীয়তাগুলি এনকোড করে, যেমন "প্রতিটি একচেটিয়া খেলোয়াড় অসীম ঘন ঘন 'গো' পাস করে"; সিটিএল একটি সিস্টেমের রাজ্য সম্পর্কে প্রয়োজনীয়তাগুলি এনকোড করে, যেমন "যে কোনও অবস্থান থেকে, সমস্ত খেলোয়াড় শেষ পর্যন্ত 'গো'-তে অবতরণ করতে পারে। সিটিএল * সূত্র, যা দুটি ব্যাকরণকে একত্রিত করে, তাও সংজ্ঞায়িত করা হয়। এই যুক্তিতে মডেল-চেকিং সূত্রের জন্য অ্যালগরিদম দেওয়া আছে। সপ্তম অধ্যায়টি দ্বি-অনুকরণের মতো রূপান্তর ব্যবস্থার তুলনা করার আনুষ্ঠানিক উপায়গুলি অন্বেষণ করে; অষ্টমটি আংশিক ক্রম হ্রাস সম্পর্কে যা একটি মডেলের বৈশিষ্ট্য যাচাই করার জন্য প্রয়োজনীয় গণনা হ্রাস করার লক্ষ্য রাখে। নবম এবং দশম অধ্যায়গুলি পূর্বে বিবেচিত যুক্তি এবং স্বয়ংক্রিয়তার সম্প্রসারণ সম্পর্কে, যার মধ্যে একটি ঘড়ির গতি (সময়োপযোগী স্বয়ংক্রিয়) বা সম্ভাব্যতা (মার্কভ চেইনের উপর ভিত্তি করে সম্ভাব্য স্বয়ংক্রিয়) যোগ করা রয়েছে। রিসেপশন ফ্রাঁসোয়া লারোসিনি দ্য কম্পিউটার জার্নালে লিখেছেন, বইটিকে "চিত্তাকর্ষক" বলে অভিহিত করে গবেষক, প্রভাষক, শিক্ষার্থী এবং প্রকৌশলীদের কাছে বইটি সুপারিশ করেছেন। লারুসিনি পাঠ্যপুস্তকটিকে ব্যাপক এবং সহজলভ্যভাবে লিখিত বলে মনে করেন, যার মধ্যে বেশ কয়েকটি উদাহরণ, অনুশীলন এবং মূল ধারণার জন্য অনুপ্রেরণামূলক ধারণা রয়েছে। একটি "সমন্বিত কাঠামো" সহ, প্রথম সাতটি অধ্যায় শাস্ত্রীয় তত্ত্বকে অন্তর্ভুক্ত করে এবং শেষ তিনটি অধ্যায় মডেল চেকিংয়ের সম্প্রসারণকে অন্তর্ভুক্ত করে। এসিএম কম্পিউটিং রিভিউতে গ্যাব্রিয়েল সিওবানু বিশ্বাস করেছিলেন যে পাঠ্যপুস্তকটি উন্নত স্নাতক বা স্নাতক কোর্সে ব্যবহার করা যেতে পারে এবং গবেষকদের জন্য কার্যকর হবে। সিওবানু "স্পষ্ট এবং স্বজ্ঞাত" উপস্থাপনার প্রশংসা করেছেন এবং বলেছেন যে "মৌলিক ধারণা, গভীর তাত্ত্বিক ফলাফল এবং মডেল চেকিং গবেষণার উন্নত বিষয়গুলি অন্তর্ভুক্ত করার জন্য এর শিক্ষামূলক পদ্ধতির জন্য প্রশংসা করা উচিত"। 2014 সালে, বইটি বুক সাইটেশন ইনডেক্স (বি. কে. সি. আই) দ্বারা পর্যবেক্ষণ করা পাঁচটি সর্বাধিক উদ্ধৃত একাডেমিক গ্রন্থের মধ্যে একটি ছিল। তথ্যসূত্র আরও পড়া বাহ্যিক লিঙ্ক অফিসিয়াল ওয়েবসাইট 2008 অ-কথাসাহিত্য বই কম্পিউটার বিজ্ঞান পাঠ্যপুস্তক