الاستدلال الآلي: الفحص الرمزي للنماذج

تقدم هذه الدورة مفهوم الفحص الرمزي للنماذج، حيث يتم التحقق التلقائي من خصائص الأنظمة والبرامج عبر نماذج الحالة والانتقال. تشرح كيفية وصف الخصائص باستخدام منطق شجرة الحسابات CTL، مع التحدي الناتج عن اتساع مساحة الحالة. لتعزيز الفحص، تُستخدم طرق التمثيل الرمزي، وخاصة الرسوم الثنائية للقرار (BDDs)، لتمثيل مجموعات الحالات بطريقة مضغوطة وفعالة. يتم شرح التعريفات، الخصائص، والخوارزميات الأساسية المتعلقة بهذه الهياكل لدعم التحقق من نماذج CTL بطريقة عملية وعلمية دقيقة.

• تعريف أنظمة الانتقال وتمثيلها الرمزي
• تطبيق منطق CTL لوصف خصائص الأنظمة
• استخدام الرسوم الثنائية للقرار (BDDs) في التحقق الرمزي
• تنفيذ خوارزميات التحقق الرمزي للنماذج

• فهم أساسي في المنطق والبرمجة على المستوى الجامعي
• الاستعداد للممارسة العملية