6.3.3.2. הגדרה אינדוקטיבית של
נגדיר סמנטיקה עבור נוסחאות CTL*
באינדוקציה על מבנה הנוסחה.
סימונים בהגדרה:
- נוסחאות מצב.
- נוסחאות מסלול.
נוסחאות מצב:
עבור ![plot:$p \in L\left( S \right) \Leftrightarrow p \in AP$](/documentResources/326/plot_1063.png)
![plot:$S\not \vDash f \Leftrightarrow S \vDash \neg
f$](/documentResources/326/plot_1064.png)
או ![plot:$S \vDash {f_1}$](/documentResources/326/plot_1066.png)
קיים מסלול
מ-
כך ש- ![plot:$\pi
\vDash {g_1}$](/documentResources/326/plot_1070.png)
נוסחאות מסלול:
כאשר
המצב הראשון ב-![plot:$\pi $](/documentResources/326/plot_1073.png)
![plot:$\pi \not \vDash
{g_1} \Leftrightarrow \pi \vDash
\neg {g_1}$](/documentResources/326/plot_1074.png)
או ![plot:$\pi
\vDash {g_1}$](/documentResources/326/plot_1076.png)
![plot:${\pi ^1} \vDash {g_1} \Leftrightarrow \pi \vDash X{g_1}$](/documentResources/326/plot_1077.png)
קיים
כך ש:
,
לכל ![plot:$0 \leqslant j < k$](/documentResources/326/plot_1082.png)
קיצורים:
(אופרטורים המוגדרים בעזרת האופרטורים הבסיסיים)
הארה
נסתכל על הקיצור האחרון
. האם היינו יכולים לכתוב אותו בעזרת Until?
כיוון אפשרי יכל להיות
אך זה איננו כיוון טוב – כי U מבטיח
שבהכרח false יתקיים בסופו של דבר. האופרטור weak-until (הידוע גם בכינויו unless)
היה יכול להתאים:
. אם weak-until היה חלק מהבסיס זו היתה הגדרה
נכונה.