6.3.4. CTL
CTL הינה לוגיקה טמפורלית נוספת, שהיא למעשה תת שפה של CTL*: CTL
מוגדרת מעל נוסחאות מצב בלבד. CTL היא השפה המוגדרת ע"י:
- אם
אז
נוסחת CTL.
- אם
נוסחאות CTL אז
נוסחאות CTL.
סמנטיקה ישירה של נוסחאות CTL:
(מעל מבנה M ומצב S)
![plot:$p \in L\left( S \right) \Leftrightarrow
S \vDash p$](/documentResources/326/plot_1117.png)
![plot:$S\not \vDash f \Leftrightarrow S \vDash \neg
f$](/documentResources/326/plot_1118.png)
או ![plot:$S \vDash f$](/documentResources/326/plot_1120.png)
קיים
כך ש-
ו-![plot:$S' \vDash f$](/documentResources/326/plot_1124.png)
ניסוח חלופי:
קיים מסלול
ממצב
כך שמתקיים
. נשים לב כי f היא נוסחת מצב. ב-CTL* הביטוי
היה מתפרש שונה.
קיים מסלול
מ-
כך שקיים
כך ש-
ולכל
.
קיים מסלול
מ-
כך שלכל
![plot:${S_i} \vDash f$](/documentResources/326/plot_1140.png)
קיצורים:
![plot:$AX{f_1} \equiv \neg EX\neg {f_1}$](/documentResources/326/plot_1141.png)
![plot:$EF{f_1} \equiv E\left(
{true\,\,U{f_1}} \right)$](/documentResources/326/plot_1142.png)
![plot:$AG{f_1} \equiv \neg EF\neg {G_1}$](/documentResources/326/plot_1143.png)
![plot:$AF{f_1} \equiv \neg EG\neg {f_1}$](/documentResources/326/plot_1144.png)
![plot:$A\left( {{f_1}U{f_2}} \right)
\equiv \neg \left( {EG\neg {f_2}\, \vee \,\,E\left( {\neg {f_2}U\left(
{\neg {f_1} \wedge \neg {f_2}} \right)} \right)} \right)$](/documentResources/326/plot_1145.png)
המצבים עבורם
לא מתקיים (אף פעם לא
מתקיים
, או שקיים מצב בו
לא מתקיים לפני ש-
התקיים)
דגשים:
- נשים לב שבמקרה של CTL יש צורך ב-3 אופרטורים טמפורליים כדי להגדיר
את האופרטורים האחרים.
- קל לזהות נוסחת CTL על ידי המבנה שלה. ב-CTL הנוסחאות מורכבות מצמדים
שהם הרכבה של כמת מסלול (E, A) ואופרטור טמפורלי (G,
F, U, X),
למשל: EF, AG וכו'.
דוגמא
אילו מהמבנים הבאים הם מודלים לנוסחה,
כלומר מספקים את הנוסחה?
הנוסחה היא:
![plot:$\begin{gathered}
AP = \left\{ {p,m,q} \right\} \hfill \\
\varphi = A\left( {pU\left(
{E\left( {qUm} \right)} \right)} \right) \hfill \\
\end{gathered} $](/documentResources/326/plot_1150.png)
אבחנה: נשים לב שזו נוסחת CTL –
האופרטורים מופיעים בה בזוגות.
מבנה ראשון:
המבנה מספק את הנוסחה. מתקיים ומכאן ![plot:$S \vDash
E\left( {qUm} \right)$](/documentResources/326/plot_1152.png)
ולכן מתקיים גם . |
![](/documentResources/326/image051.png) |
מבנה שני:
המבנה מספק את הנוסחה. חשוב לשים לב שכל הנוסחאות הן נוסחת מצב - אפשר לסמן בכל מצב את
הנוסחאות אותן הוא מספק. |
![](/documentResources/326/image053.png) |