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

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

6.3.3.1. הגדרת CTL*

CTL* הינה סוג של לוגיקה טמפורלית, המוגדרת באמצעות 2 סוגי נוסחאות:

נוסחאות מצב שמתפשרות במצב נתון.
נוסחאות מסלול שמתפרשות במסלול נתון.

הגדרה אינדוקטיבית של הלוגיקה:

נוסחאות מצב

בסיס: נוסחאות אטומיות $plot:$p \in AP$$ .
כללי יצירה:

אם נוסחאות מצב אז $plot:$\neg f\,,\,f \vee g$$ הן נוסחאות מצב.
אם נוסחת מסלול אז היא נוסחת מצב.

נוסחאות מסלול

בסיס: כל נוסחת מצב היא נוסחת מסלול. (הנוסחה תבחן על המצב הראשון במסלול).
כללי יצירה: אם נוסחאות מסלול אז $plot:$fUg,Xf,\neg f,f \vee g$$ הן נוסחאות מסלול.

CTL* היא קבוצת נוסחאות המצב המוגדרות לפי הגדרה זו. נסביר זאת: CTL* מוגדרת באופן אינדוקטיבי באמצעות נוסחאות מצב ונוסחאות מסלול. נוסחאות המסלול משמשות אותנו להגדרת קבוצת הנוסחאות CTL* (כצעד ביניים), אך הבנייה לעולם לא עוצרת כשיש לנו ביד נוסחת מסלול.

הערות להגדרה האינדוקטיבית:

חשוב לשים לב: כל נוסחה אטומית ב-AP היא נוסחת מצב של CTL*.
המסלול מספק נוסחת מצב אם המצב הראשון במסלול מספק את הנוסחה.
שאלה: האם ניתן לעשות $plot:$ \vee $$ בין נוסחת מצב לנוסחת מסלול? לפי ההגדרה – כן, כי כל נוסחת מצב היא נוסחת מסלול. $plot:${\varphi _1}$$ נוסחת מצב, $plot:${\varphi _2}$$ נוסחת מסלול, אזי לפי הבסיס $plot:${\varphi _1}$$ היא גם נוסחת מסלול ו- $plot:${\varphi _1} \vee {\varphi _2}$$ היא נוסחת מסלול.

נוסחאות CTL* מתפרשות מעל מבנה קריפקה plot:$M$ : $plot:$M = \left( {S,R,L,{S_0}} \right)$$ . $plot:${S_0}$$ הינו אופציונלי בלבד.

הגדרה: מסלול ב- plot:$M$ ממצב plot:$S$ הינו סדרה אינסופית $plot:${S_0},{S_1},{S_2},...$$ כך שלכל $plot:\[i \geqslant 0\]$ , מתקיים $plot:\[\left( {{S_i},{S_{i + 1}}} \right) \in R\,\]$ ובנוסף $plot:${S_0} = S$$ .

סימונים:

$plot:${\pi ^j}$$ - הסיפא של $plot:$\pi $$ ממצב $plot:${S_j}$$ ( $plot:${\pi ^0}$$ - כל המסלול)

סמנטיקה:

$plot:$M,S \vDash f$$ - אם נוסחת מצב נכונה במבנה במצב.
$plot:$M,\pi \vDash f$$ - אם נוסחת מסלול הנכונה במבנה במסלול $plot:$\pi $$ .
$plot:$M \vDash f$$ אם כוללת הגדרת $plot:${S_0}$$ ולכל $plot:${s_0} \in {S_0}$$ $plot:$M,{s_0} \vDash f$$ .