הועלה לאתר:  
מספר עמודים: 120
הורדת המסמך בגרסה להדפסהלהורדת המסמך בשלמותו

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

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

7.4.1. CTL*

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

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

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

נוסחאות מצב

  1. בסיס: נוסחאות אטומיות plot:$p \in AP$.
  2. כללי יצירה:
  • אם plot:$f,g$ נוסחאות מצב אז plot:$\neg f\,,\,f \vee g$ הן נוסחאות מצב.
  • אםplot:$f$ נוסחת מסלול אזplot:$Ef$ היא נוסחת מצב.

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

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

CTL* היא קבוצת נוסחאות המצב המוגדרות לפי הגדרה זו.



קיצורים: (אופרטורים המוגדרים בעזרת האופרטורים הבסיסיים)

  • plot:${f_1} \wedge {f_2} \equiv \neg \left( {\neg {f_1} \vee \neg {f_2}} \right)$
  • plot:${g_1} \wedge {g_2} \equiv \neg \left( {\neg {g_1} \vee \neg {g_2}} \right)$
  • plot:$Af \equiv \neg E\neg f$
  • plot:$Ff \equiv \left( {true\,Uf} \right)$
  • plot:$Fg \equiv \left( {true\,Ug} \right)$
  • plot:$Gg \equiv \neg F\neg g$

תגיות המסמך:

לפרק הקודם7.4. לוגיקות טמפורליות
לפרק הבא7.4.2. CTL
אין תגובות!
שיתוף:
| עוד