מבוא לאימות תוכנה

ספר אלקטרוני מאת: ניר אדר

6.7.4.1. תרגיל 1

בשאלה זו נדון באלגוריתם Bounded Model Checking (BMC) לבדיקת $plot:\[AGp\]$ .

סעיף א'

נתון מבנה קריפקה $plot:\[M\]$ שמיוצג ע"י נוסחאות CNF. בעת חישוב הנוסחה עבור רלציית המעברים $plot:\[R\]$ קרתה "תקלה" וחלק מהפסוקיות בנוסחת ה- CNF הושמטו. נסמן את הנוסחה שהתקבלה ב- $plot:\[{R_1}\]$ . נריץ בדיקת ספיקות של נוסחה $plot:\[\phi \]$ שהיא נוסחת BMC עבור $plot:\[M\]$ , $plot:\[k\]$ ו- $plot:\[AGp\]$ תוך שימוש ב- $plot:\[{R_1}\]$ במקום $plot:\[R\]$ . האלגוריתם מחזיר "sat" (כלומר – הנוסחה סופקה). האם $plot:\[M\mathop {| \ne }\limits_k AGp\]$ ?

פתרון סעיף א':

לא בהכרח - אם מורידים פסוקיות מנוסחה שמייצגת קשת בגרף, עלולים ליצור קשתות נוספות ובכך לאפשר מסלולים שלא היו קיימים וכך למצוא מסלול שסותר את plot:$AGp$ .

הדגש החשוב (והמבלבל בתחילה) בדרך להבנה: מחיקת פסוקיות יוצרת מסלולים חדשים המקיימים את הנוסחה. נסו למחוק בדוגמת ה-shift register את אחת הפסוקיות כדי להבין זאת.

סעיף ב'

האלגוריתם מחזיר "unsat". האם בהכרח $plot:\[M\mathop {| = }\limits_k AGp\]$ ?

פתרון סעיף ב':

מתקיים $plot:\[M\mathop {| = }\limits_k AGp\]$ - הוספנו עוד מסלולים לגרף. אם לא הצלחנו לספק את הנוסחה עם מסלולים נוספים, אין סיכוי שנצליח לספק אותה עם פחות מסלולים. לכן בכל המסלולים יתקיים plot:$AGp$ .

סעיף ג'

הפעם בעת חישוב הנוסחה עבור $plot:\[R\]$ נוספו פסוקיות CNF. נוסחת ה- BMC שהתקבלה מסומנת

ב- $plot:\[{R_2}\]$ והאלגוריתם לבדיקת ספיקות השתמש בה במקום ב-R.

אם מתקיים כי האלגוריתם מחזיר "sat", האם $plot:\[M\mathop {| \ne }\limits_k AGp\]$ ? ואם מתקיים כי האלגוריתם מחזיר "unsat", האם $plot:\[M\mathop {| = }\limits_k AGp\]$ ?