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

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

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

7.4.2. CTL

CTL היא השפה המוגדרת ע"י:

  1. אםplot:\[p \in AP\]  אזplot:$p$ נוסחת CTL.
  2. אםplot:$f,g$ נוסחאות CTL אז plot:$\neg f,f \vee g\$E\left( {fUg} \right),\,EXg,\,EGg$ נוסחאות CTL.

קיצורים:

  • plot:$AX{f_1} \equiv \neg EX\neg {f_1}$
  • plot:$EF{f_1} \equiv E\left( {true\,\,U{f_1}} \right)$
  • plot:$AG{f_1} \equiv \neg EF\neg {G_1}$

תגיות המסמך:

לפרק הקודם7.4.1. CTL*
לפרק הבא7.4.3. LTL
אין תגובות!
שיתוף:
| עוד