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

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

6.4.1. הבעיה והאלגוריתם

בדיקת מודל מפורשת (Explicit model checking) היא אלגוריתם המבצע בדיקת מודל, העובד ישירות על הגרף - מבנה קריפקה. המודל M נתון באופן מפורש כייצוג של הגרף – וממומש לרוב כמטריצת סמיכויות או כרשימת בנים.

האלגוריתם המפורש הוא קל להבנה, אך בעייתי למימוש עקב "בעיית התפוצצות המצבים": במערכת בה plot:$n$ משתנים בוליאנים, יהיו $plot:${2^n}$$ מצבים אפשריים למערכת. מספר המצבים השונים גדל מהר מאוד כאשר המערכת גדלה, וכמות הזכרון לא מספיקה לייצוג מלא של המודל.

כדי לפתור את בעיה זו נציג בהמשך 2 אלגוריתמים אחרים שהם אלגוריתמים סימבוליים – אנו נציג קידוד של המבנה M וגם של תוצאות הביניים המאפשר שימוש בפחות זכרון.

האלגוריתם לבדיקת מודל CTL מטפל בנוסחאות מהצורה: $plot:$EGf,EFf,E\left( {fUg} \right),\,\,EXf\$\neg f,\,\,f \vee g,\,\,a \in AP$$ כאשר f, g הן נוסחאות CTL. אם נרצה להתאים את האלגוריתם לאופרטורים נוספים – נצטרך לפתח עבורם אלגוריתמים, או לחילופין לתרגם את האופרטורים הנוספים לאופרטורים אלה.

תיאור כללי של האלגוריתם:

נצרף לכל מצב plot:$S$ משתנה $plot:$label\left( S \right)$$ שיחזיק קבוצה של תתי נוסחאות של plot:$f$ שנכונות ב-.

טיפול בתת נוסחה: $plot:$M,S \vDash g \Leftrightarrow f \in \,\,label\left( S \right)$$
בסיום האלגוריתם $plot:$M,S \vDash f \Leftrightarrow f \in \,\,label\left( S \right)$$ . נקבל את $plot:${S_f} = \left\{ {S|f \in \,\,label\left( S \right)} \right\}$$ קבוצת המצבים שבהם הנוסחה נכונה.

האלגוריתם עובד באיטרציות על תתי הקבוצות של plot:$f$ מהנוסחאות האטומיות אל הנוסחאות המורכבות יותר, על כל תתי הקבוצות של .

דוגמא לסדר הטיפול: עבור הנוסחה הבאה $plot:$f = \left( {\neg b \vee c} \right) \vee EG\left( {EXa \vee \neg b} \right)$$

איטרציה 1: נטפל בנוסחאות האטומיות:
איטרציה 2: $plot:$\neg b,EXa$$
איטרציה 3: $plot:$\neg b \vee c,EXa \vee \neg b$$
איטרציה 4: $plot:$EG\left( {EXa \vee \neg b} \right)$$
איטרציה 5:

בעמודים הבאים נציג מה הפירוש של "טיפול בתת נוסחה plot:$g$ " שהוזכר בתיאור האלגוריתם.

בכל איטרציה plot:$g$ יהיה תת הנוסחה איתה אנו מתעסקים.

האלגוריתם לסימון:

צעד 0: נוסחאות אטומיות $plot:$\left( {g \in AP} \right)$$

לכל $plot:$s \in S$$ , $plot:$label\left( s \right): = L\left( s \right)$$ .

סיבוכיות: $plot:$0\left( {|S|} \right)$$

צעד זה הוא היחיד שלא קשור לנוסחה plot:$g$ בה אנו מטפלים כרגע. בתחילת ריצת האלגוריתם

נסמן כל מצב בנוסחאות האטומיות המספקות אותו.

צעד 1:

סימון ב- $plot:$\neg g$$

לכל $plot:$s \in S$$ :

$plot:$if\,\,\,g \notin label\left( s \right)\,\,\,\,then\,\,\,label\left( s \right): = label\left( s \right) \cup \left\{ {\neg g} \right\}$$

סיבוכיות: $plot:$0\left( {|S|} \right)$$

סימון ב- $plot:$g = {f_1} \vee {f_2}$$

לכל $plot:$s \in S$$ :

$plot:$if\,\,\,{f_1} \in label\left( s \right)\,\,\,\,or\,\,\,{f_2} \in label\left( s \right)\,\,then$$

$plot:$label\left( s \right): = label\left( s \right) \cup \left\{ {{f_1} \vee {f_2}} \right\}$$

סיבוכיות: $plot:$0\left( {|S|} \right)$$

סימון ב- $plot:$g = EX{f_1}$$

לכל מצב plot:$s$ :

$plot:$if\,\,\,\exists s'\left( {\left( {s,s'} \right) \in R \wedge {f_1} \in label\left( {s'} \right)} \right)\,\,then$$ $plot:$label\left( s \right): = label\left( s \right) \cup \left\{ {EX{f_1}} \right\}$$

פירוש: קיימת קשת מצומת האב לצומת אחר, וגם מתקיים $plot:${f_1}$$ בצומת הבן.

סיבוכיות $plot:$0\left( {|S| + |R|} \right)$$

האלגוריתם לסימון $plot:$g = E\left( {{f_1}U{f_2}} \right)$$

מצאו את כל המצבים שמסומנים ב- $plot:${f_2}$$ וסמנו אותם ב-. נכניס את המצבים לקבוצה T ונסמן אותם כ-visit.

כלומר, לכל $plot:$s \in S$$ :

$plot:\[if\,\,{f_2} \in label\left( s \right)\,\,\,then\,\]$

$plot:\[label\left( s \right): = label\left( s \right) \cup \left\{ g \right\}\]$

$plot:$visit\left( s \right) = true$$

$plot:$T: = T \cup \left\{ s \right\}$$

המטרה שלנו: סריקה אחורנית של הגרף החל מכל מצב שסומן ב- וסימון כל מצב שיש לו בן שמסומן ב- והוא עצמו מסומן ב- $plot:${f_1}$$ , ב-. אנו מבצעים סריקה אחורנית על מנת לא לסגור מעגל.

שלבי הפעולה:

נבחר $plot:$s \in T$$ ונוציאו מ-.
לכל המקיים $plot:$R\left( {t,s} \right) \wedge \neg visit\left( t \right)$$ ( אב של אותו עדיין לא ביקרנו), אם מתקיים $plot:${f_1} \in label\left( t \right)$$ :

$plot:$label\left( t \right): = label\left( t \right) \cup \left\{ g \right\}$$
$plot:$T: = T \cup \left\{ t \right\}$$

עוצרים כאשר ריקה.

ניסוח חלופי לאלגוריתם צעד-צעד להבהרת הפעולה:

$plot:$if\,\,\,g \in label\left( s \right) \wedge \left( {t,s} \right) \in R \wedge {f_1} \in label\left( t \right)\,\,then\,\,\,label\left( t \right): = label\left( t \right) \cup \left\{ g \right\}$$

האלגוריתם מסתמך על השקילות הבאה: $plot:$E\left( {{f_1}U{f_2}} \right) = {f_2} \vee \left( {{f_1} \wedge EXE\left( {{f_1}U{f_2}} \right)} \right)$$

סיבוכיות האלגוריתם: $plot:$O\left( {|S| + |R|} \right)$$

הערות על האלגוריתם:

מעגלים בגרף "לא נכנסים למשחק". אנחנו בוחנים רק מצבים שיש מהם דרך ל- $plot:${f_2}$$ . (הסריקה האחורנית דואגת לכך).
הסימון ב-visit מונע סריקות מיותרות של העץ. על ידי סימון זה אנחנו משיגים את הסיבוכיות הליניארית של האלגוריתם.
בסוף האלגוריתם המצבים המסומנים הם מצבים שיש להם מסלול סופי אל $plot:${f_2}$$ וגם מקיימים את התנאי.

דוגמא:

שלב ראשון: מסומנים ב- $plot:\[{f_2}\]$ : $plot:${S_1},{S_4},{S_8}$$ .

שלב שני: האבות שלהם:

אנחנו לא מסמנים את $plot:${S_2}$$ כי הוא אינו מסומן ב- $plot:${f_1}$$ .

שלב שלישי: האבות של האבות:

אנו לא מסמנים ולא מטפלים שוב במצבים שכבר סומנו ( $plot:${S_4},{S_5}$$ ).

ולבסוף:

מתקבל בסוף: $plot:${S_{E\left( {{f_1}U{f_2}} \right)}} = \left\{ {{S_1},{S_3},{S_4},{S_5},{S_6},{S_8}} \right\}$$

האלגוריתם לסימון $plot:$g = EG{f_1}$$

הגדרות: רכיב קשיר היטב: (SCC) – Strongly Connected Component הינו תת גרף C, שבו מכל צומת יש מסלול לכל צומת ב-C, דרך צמתים ב-C.

רכיב קשיר היטב הוא טריוויאלי אם הוא מורכב מצומת בודד ללא חוג עצמי.
רכיב קשיר היטב הוא מקסימאלי (MSCC) אם אינו מוכל ממש ברכיב קשיר היטב אחר. תכונה חשובה של רכיבים מקסימליים: אם $plot:${C_1},{C_2}$$ שניהם MSCC, אזי $plot:${C_1} \cap {C_2} = \emptyset $$ .
רכיבים קשירים היטב מקסימאליים הם זרים ולכן סכום הצמתים בהם הוא $plot:$\left| S \right|$$ . סכום הצמתים ברכיבים קשירים היטב לא בהכרח מקסימאליים הוא $plot:${2^{\left| S \right|}}$$ .

דוגמא:

$plot:\[SCC = \left\{ {\left\{ 1 \right\},\left\{ 2 \right\},\left\{ 3 \right\},\left\{ 4 \right\},\left\{ 5 \right\},\left\{ {4,5} \right\},\left\{ {3,4,5} \right\}} \right\}\]$

רכיבים קשירים היטב מקסימאליים: $plot:$\left\{ {\left\{ {3,4,5} \right\},\left\{ 2 \right\}} \right\}$$
רכיבים קשירים היטב טריוויאליים: $plot:$\left\{ {\left\{ 1 \right\},\left\{ 3 \right\},\left\{ 4 \right\},\left\{ 5 \right\}} \right\}$$ .

האלגוריתם של Tarjan מוצא את כל הרכיבים המקסימאליים בסיבוכיות $plot:$O\left( {\left| S \right| + \left| R \right|} \right)$$ (כולל רכיבים טריויאליים).

נגדיר את המבנה המצומצם הבא: בהינתן $plot:$M = \left( {S,R,L} \right)$$ נגדיר $plot:$M' = \left( {S',R',L'} \right)$$ ע"י:

$plot:$S' = \left\{ {S|M,S \vDash {f_1}} \right\}$$
$plot:$R' = \left( {S' \times S'} \right) \cap R$$ הערה: אינה בהכרח טוטאלית
$plot:$ \leftarrow L' = L|S'$$ הטלה של על

נסתמך על המשפט הבא:

משפט: $plot:$ \Leftrightarrow M,s \vDash EG{f_1}$$

$plot:$s \in S'$$
קיים מסלול ב- ממצב למצב ברכיב קשיר היטב מקסימאלי לא טריוויאלי של .

המשפט מבטיח לנו שקיים מסלול אינסופי בו מסתפק $plot:${f_1}$$ (ולא רק רישא סופית שבה הוא מסתפק).

האלגוריתם עצמו:

בונים $plot:$M' = \left( {S',R',L'} \right)$$ כמתואר לעיל. $plot:$O\left( {\left| S \right| + \left| R \right|} \right)$$
מוציאים את כל הרכיבים הקשירים היטב המקסימאליים ב-. $plot:$O\left( {\left| S \right| + \left| R \right|} \right)$$
כל מצב ברכיב קשיר היטב לא טריוויאלי יסומן ב-. $plot:$O\left( {\left| S \right|} \right)$$
מכל מצב שמסומן ב- נבצע סקירה אחורנית ב- ונסמן כל מצב שממנו יש מסלול לרכיב קשיר היטב. $plot:$O\left( {\left| S \right| + \left| R \right|} \right)$$