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

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

6.5.6. יצוג מבנה קריפקה בעזרת BDD

BDD זו דרך שימושית לייצג יחסים על פני תחום סופי. נראה כיצד ניתן לייצג את מכונת קריפקה באמצעות BDD. שיטת העבודה בה נשתמש: נניח ש- plot:$Q$ זו רלציה plot:$n$ -ממדית מעל $plot:$\left\{ {0,1} \right\}$$ אזי יכולה להיות מיוצגת על ידי ה-BDD עם הפונקציה האופיינית הבאה:

$plot:${f_Q}\left( {{x_1},...,{x_n}} \right) = 1 \Leftrightarrow Q\left( {{x_1},...,{x_n}} \right)$$

אחרת תהא plot:$Q$ רלציה plot:$n$ -ממדית מעל תחום סופי plot:$D$ . ללא הגבלת כלליות, נניח שב- ישנם $plot:${2^m}$$ אלמנטים ( plot:$m > 1$ ). על מנת לייצג את כ-BDD, נקודד את האלמנטים של על ידי הטרנספורמציה $plot:$\phi :{\left[ {0,1} \right]^m} \to D$$ שממפה כל ווקטור בוליאני באורך plot:$m$ אל אלמנט ב- plot:$D$ . על ידי שימוש בקידוד $plot:$\phi $$ נוכל לבנות רלציה בינארית $plot:$\hat Q$$ כך:

$plot:$\hat Q\left( {{{\tilde x}_1},...,{{\tilde x}_n}} \right) = Q\left( {\phi \left( {{{\tilde x}_1}} \right),...,\phi \left( {{{\tilde x}_n}} \right)} \right)$$

כאשר $plot:${\tilde x_i}$$ הוא ווקטור של plot:$m$ משתנים בוליאניים שמקודדים את המשתנה $plot:${x_i}$$ שהינו ערך מ- plot:$D$ .

מכונת קריפקה כאמור הינה $plot:$M = \left( {S,R,L} \right)$$ . כדי לייצג את המכונה במלואה צריכים להציג את הקבוצה plot:$S$ , את הרלציה plot:$R$ ואת פונקצית הסימון plot:$L$ .

כדי לייצג את plot:$S$ צריכים פונקציית קידוד. לצורת הנוחות נניח $plot:${2^m}$$ מצבים, ואז כמו עבור הרלציה נגדיר פונקצית מיפוי בוליאנית $plot:$\phi :{\left[ {0,1} \right]^m} \to S$$ . ה-BDD המתאים מורכב בצורה דומה לקודם.

הרלציה plot:$R$ מורכבת מאותו הקידוד, כאשר אנחנו משתמשים בשני סטים מקבילים של משתנים בוליאניים כדי להציג את המצב לפני ואת המצב לאחר המעבר $plot:$\hat R\left( {\tilde x,\tilde x'} \right)$$ .

בעניין פונקצית המיפוי plot:$L$ , למרות שהפונקציה מוגדרת בתוך מיפוי מקבוצת המצבים אל תת קבוצה של הנוסחאות האטומיות, יותר נוח לנו להסתכל על הפונקציה כמיפוי מנוסחאות אטומיות לתת קבוצה של מצבים. הנוסחה האטומית plot:$p$ ממופה לקבוצת המצבים המספקים אותה: $plot:$\left\{ {s|p \in L\left( s \right)} \right\}$$ . אם נסמן קבוצה זו ב- $plot:${L_p}$$ , נוכל להציג אותה באמצעות הקידוד $plot:$\phi $$ כמו שהצגנו קודם. באופן כזה, נוכל להציג כל אחד מהביטויים האטומיים. כלומר:

לכל נוסחה אטומית $plot:$a \in AP$$ נקבל את ה-BDD שמייצג את קבוצת המצבים המספקים את plot:$a$ ונסמנו ב- $plot:$a\left( {\bar v} \right)$$ .

לפרק הקודם6.5.5.4. פעולת not

לפרק הבא6.6. בדיקת מודל סימבולית מבוססת BDD

תגובות:

שם:	(התחברות)
נושא:
תוכן:
	אין לשלוח תגובות הכוללות מידע המפר את תנאי השימוש של אתר UnderWarrior לרבות דברי הסתה, דיבה וסגנון החורג מהטעם הטוב.
		אימות: