Kripke structure (model checking)
یہ مضمون کرپکے ڈھانچے کو بیان کرتا ہے جیسا کہ ماڈل چیکنگ میں استعمال ہوتا ہے۔ مزید عمومی وضاحت کے لیے، کرپکے سیمنٹکس دیکھیں۔ کرپکے ڈھانچہ منتقلی کے نظام کا ایک تغیر ہے، جسے اصل میں ساؤل کرپکے نے تجویز کیا تھا، جو کسی نظام کے رویے کی نمائندگی کے لیے ماڈل چیکنگ میں استعمال ہوتا ہے۔ یہ ایک گراف پر مشتمل ہوتا ہے جس کے نوڈس نظام کی قابل رسائی حالتوں کی نمائندگی کرتے ہیں اور جس کے کنارے ریاستی منتقلی کی نمائندگی کرتے ہیں، ایک لیبلنگ فنکشن کے ساتھ جو ہر نوڈ کو متعلقہ حالت میں موجود خصوصیات کے ایک سیٹ سے نقشہ بناتا ہے۔ عارضی منطقوں کی روایتی طور پر تشریح کرپکے ڈھانچے کے لحاظ سے کی جاتی ہے۔ رسمی تعریف آئیے جوہری تجاویز کا ایک مجموعہ ہوں، یعنی۔ بولین قدر والے تاثرات متغیرات، مستقل اور پیش گوئی کی علامتوں سے تشکیل پاتے ہیں۔ کلارک اور دیگر۔ کرپکے ڈھانچے کو 4-ٹپل کے طور پر بیان کریں جو ریاستوں کے ایک محدود سیٹ پر مشتمل ہے۔ ابتدائی ریاستوں کا ایک مجموعہ۔ ایک منتقلی کا رشتہ ایسا جو بائیں کل کا ہو، یعنی ایسا۔ لیبلنگ (یا تشریح) فنکشن۔ چونکہ یہ مکمل طور پر بچا ہوا ہے، اس لیے کرپکے ڈھانچے کے ذریعے ایک لامحدود راستہ بنانا ہمیشہ ممکن ہے۔ ڈیڈ لاک اسٹیٹ کو ایک واحد باہر جانے والے کنارے کے ذریعے خود ہی ماڈل کیا جا سکتا ہے۔ لیبلنگ فنکشن ہر ریاست کے لیے تمام جوہری تجاویز کے سیٹ کی وضاحت کرتا ہے جو اس میں درست ہیں۔ ساخت کا راستہ ریاستوں کا ایک سلسلہ ہے جو ہر ایک کے لیے برقرار رہتا ہے۔ راستے پر موجود لفظ جوہری تجاویز کے سیٹوں کی ترتیب ہے، جو حروف تہجی پر ایک ω-لفظ ہے۔ اس تعریف کے ساتھ، ایک کرپکے ڈھانچہ (جیسے، صرف ایک ابتدائی حالت رکھنے والی مور مشین کے ساتھ سنگلٹن ان پٹ حروف تہجی کے ساتھ شناخت کی جا سکتی ہے، اور آؤٹ پٹ فنکشن اس کی لیبلنگ فنکشن ہے۔ مثال کے طور پر جوہری تجاویز کا مجموعہ لیں۔ اور نظام کی صوابدیدی بولین خصوصیات کا نمونہ بنا سکتا ہے جسے کرپکے ڈھانچہ ماڈلنگ کر رہا ہے۔ دائیں طرف کی شکل کرپکے ڈھانچے کی وضاحت کرتی ہے، جہاں۔ ۔ ۔ ۔ ایک راستہ پیدا کر سکتا ہے اور راستے پر عمل درآمد کا لفظ ہے۔ زبان سے تعلق رکھنے والے پھانسی کے الفاظ تیار کر سکتے ہیں۔ دیگر تصورات سے تعلق اگرچہ یہ اصطلاح ماڈل چیکنگ کمیونٹی میں وسیع پیمانے پر پھیلی ہوئی ہے، ماڈل چیکنگ پر کچھ نصابی کتابیں "کرپکے ڈھانچے" کی وضاحت اس توسیعی طریقے سے (یا حقیقت میں بالکل بھی) نہیں کرتی ہیں، بلکہ صرف ایک (لیبل شدہ) منتقلی کے نظام کے تصور کو استعمال کرتی ہیں، جس میں اضافی طور پر اعمال کا ایک مجموعہ ہوتا ہے، اور منتقلی کے تعلق کو ایک ذیلی سیٹ کے طور پر بیان کیا جاتا ہے، جس میں وہ اضافی طور پر جوہری تجاویز کا ایک مجموعہ اور ریاستوں کے لیے ایک لیبلنگ فنکشن بھی شامل کرتے ہیں (جیسا کہ اوپر بیان کیا گیا ہے)۔ اس نقطہ نظر میں، ایکشن لیبلز کو خلاصہ کرنے سے حاصل ہونے والے بائنری تعلق کو اسٹیٹ گراف کہا جاتا ہے۔ کلارک اور دیگر۔ کرپکے ڈھانچے کو ٹرانزیشن کے ایک سیٹ کے طور پر دوبارہ بیان کریں (صرف ایک کے بجائے)، جو کہ اوپر لیبل شدہ ٹرانزیشن کے مساوی ہے، جب وہ موڈل μ-کیلکولس کے الفاظ کی وضاحت کرتے ہیں۔ یہ بھی دیکھیں کہ عارضی منطق ماڈل چیکنگ کرپکے سیمنٹکس لکیری عارضی منطق کمپیوٹیشن ٹری منطق حوالہ جات ماڈل چیکنگ عارضی منطق ٹرانزیشن سسٹم