Principles of Model Checking
ماڈل چیکنگ کے اصول ماڈل چیکنگ پر ایک نصابی کتاب ہے، جو کمپیوٹر سائنس کا ایک شعبہ ہے جو اس بات کا تعین کرنے کے مسئلے کو خودکار بناتا ہے کہ آیا مشین تفصیلات کی ضروریات کو پورا کرتی ہے یا نہیں۔ اسے کرسٹل بایر اور جوسٹ پیٹر کٹوین نے لکھا تھا، اور 2008 میں ایم آئی ٹی پریس نے شائع کیا تھا۔ تعارف اور پہلا باب ماڈل چیکنگ کے شعبے کا خاکہ پیش کرتا ہے: کسی مشین یا عمل کے ماڈل کا تجزیہ یہ دیکھنے کے لیے کیا جا سکتا ہے کہ آیا مطلوبہ خصوصیات موجود ہیں یا نہیں۔ مثال کے طور پر، ایک وینڈنگ مشین اس خاصیت کو پورا کر سکتی ہے کہ "بیلنس کبھی بھی 0,00 یورو سے نیچے نہیں آسکتا"۔ ایک ویڈیو گیم اس اصول کو نافذ کر سکتا ہے کہ "اگر کھلاڑی کی زندگی 0 ہے تو کھیل نقصان میں ختم ہوتا ہے"۔ وینڈنگ مشین اور ویڈیو گیم دونوں کو ٹرانزیشن سسٹم کے طور پر بنایا جا سکتا ہے۔ ماڈل چیکنگ ریاضیاتی زبان میں اس طرح کی ضروریات کو بیان کرنے کا عمل ہے، اور خودکار ثبوت پیش کرتا ہے کہ ماڈل ضروریات کو پورا کرتا ہے، یا اگر ماڈل ناقص ہے تو جوابی مثالوں کی دریافت۔ دوسرا باب سمورتی نظاموں کے لیے ایک مناسب ماڈل بنانے پر مرکوز ہے، جہاں الگورتھم کے متعدد حصوں (ہدایات کا مجموعہ) کو مختلف مشینوں یا مشین کے حصوں کے ذریعے بیک وقت انجام دیا جا سکتا ہے۔ باب 3 ان اصولوں کی اقسام کی کھوج کرتا ہے جنہیں ایک منتقلی کا نظام پورا کر سکتا ہے: لکیری وقت کی خصوصیات۔ ایک حفاظتی خاصیت، جیسے کہ "کوئی تعطل کی حالت ممکن نہیں ہے"، اس شکل کی ہوتی ہے کہ "ایک ناپسندیدہ نتیجہ کبھی نہیں ہو سکتا"۔ ایک لائیونیس پراپرٹی، جیسے کہ "ایک مشترکہ وسائل ہمیشہ آخر کار کسی جزو کے لیے دستیاب کیا جائے گا جو اس کی درخواست کرتا ہے"، اس شکل کا ہے کہ "آخر کار ایک مطلوبہ نتیجہ سامنے آئے گا"۔ منصفانہ خصوصیات جیسے کہ "ٹریفک لائٹ کبھی رنگ بدلنا نہیں روکتی" کو پیشگی شرائط کے طور پر استعمال کیا جا سکتا ہے۔ مفروضے جن سے دیگر خصوصیات کا اندازہ لگایا جا سکتا ہے۔ چوتھا باب باقاعدہ اور ω-باقاعدہ زبان کی خصوصیات، اور نظریاتی مشینوں جیسے بوچی آٹومیٹا کے بارے میں ہے جو زبانوں کا نمونہ بناتی ہیں۔ یہ خصوصیات کی تصدیق کرنے یا جوابی مثالیں تلاش کرنے کے لیے ماڈل چیکنگ الگورتھم فراہم کرتا ہے۔ پانچویں اور چھٹے ابواب لکیری عارضی منطق (ایل ٹی ایل) اور کمپیوٹیشن ٹری منطق (سی ٹی ایل) کو تلاش کرتے ہیں، فارمولے کی دو کلاسیں جو خصوصیات کا اظہار کرتی ہیں۔ ایل ٹی ایل ایک نظام کے ذریعے راستوں کے بارے میں ضروریات کو انکوڈ کرتا ہے، جیسے کہ "ہر اجارہ دار کھلاڑی لامحدود کثرت سے 'گو' سے گزرتا ہے ؛ سی ٹی ایل ایک نظام میں ریاستوں کے بارے میں ضروریات کو انکوڈ کرتا ہے، جیسے کہ" کسی بھی پوزیشن سے، تمام کھلاڑی بالآخر 'گو' پر اتر سکتے ہیں۔ سی ٹی ایل * فارمولے، جو دونوں گرامروں کو یکجا کرتے ہیں، کی بھی وضاحت کی گئی ہے۔ ان منطقوں میں ماڈل چیک کرنے کے فارمولوں کے لیے الگورتھم دیے گئے ہیں۔ ساتواں باب منتقلی کے نظاموں کا موازنہ کرنے کے رسمی طریقوں کی کھوج کرتا ہے، جیسے کہ بائیسیمولیشن ؛ آٹھواں جزوی ترتیب میں کمی کے بارے میں ہے جس کا مقصد کسی ماڈل کی خصوصیات کی تصدیق کے لیے درکار حساب کو کم کرنا ہے۔ نویں اور دسویں ابواب ان منطقوں اور آٹومیٹا کی توسیع کے بارے میں ہیں جن پر پہلے غور کیا گیا تھا، بشمول گھڑی کی رفتار (ٹائمڈ آٹومیٹا) یا امکانات (مارکوف زنجیروں پر مبنی ممکنہ آٹومیٹا) کے اضافے کے ذریعے۔ استقبالیہ فرانسوا لاروسینی نے دی کمپیوٹر جرنل میں لکھتے ہوئے محققین، لیکچررز، طلباء اور انجینئروں کو اس کتاب کی سفارش کرتے ہوئے اسے "متاثر کن" قرار دیا۔ لاروسینی نے نصابی کتاب کو جامع اور قابل رسائی لکھا ہوا پایا، جس میں اچھی تعداد میں مثالیں، مشقیں اور کلیدی تصورات کے لیے حوصلہ افزا خیالات تھے۔ "متحد فریم ورک" کے ساتھ، پہلے سات ابواب کلاسیکی نظریہ کا احاطہ کرتے ہیں اور آخری تین ابواب ماڈل چیکنگ کی توسیع کا احاطہ کرتے ہیں۔ اے سی ایم کمپیوٹنگ ریویوز میں، گیبریل سیوبانو کا خیال تھا کہ اس نصابی کتاب کو اعلی درجے کے انڈرگریجویٹ یا گریجویٹ کورسز میں استعمال کیا جا سکتا ہے، اور یہ محققین کے لیے مفید ثابت ہوگی۔ سیوبانو نے "واضح اور بدیہی" پریزنٹیشن کی تعریف کی اور کہا کہ "ماڈل چیکنگ ریسرچ میں بنیادی تصورات، گہرے نظریاتی نتائج، اور جدید موضوعات کا احاطہ کرنے کے لیے اس کے تدریسی نقطہ نظر کی تعریف کی جانی چاہیے"۔ 2014 میں، یہ کتاب بک سائٹیشن انڈیکس (بی کے سی آئی) کے زیر نگرانی پانچ سب سے زیادہ حوالہ شدہ تعلیمی متن میں سے ایک تھی۔ حوالہ جات مزید پڑھنے بیرونی روابط سرکاری ویب سائٹ 2008 غیر افسانوی کتابیں کمپیوٹر سائنس کی نصابی کتابیں