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

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

6.3.4. CTL

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

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

סמנטיקה ישירה של נוסחאות CTL: (מעל מבנה M ומצב S)

$plot:$p \in L\left( S \right) \Leftrightarrow S \vDash p$$
$plot:$S\not \vDash f \Leftrightarrow S \vDash \neg f$$
$plot:$S \vDash g \Leftrightarrow S \vDash f \vee g$$ או $plot:$S \vDash f$$
$plot:$ \Leftrightarrow S \vDash EXf$$ קיים כך ש- $plot:$\left( {S,S'} \right) \in R$$ ו- $plot:$S' \vDash f$$

ניסוח חלופי: $plot:$ \Leftrightarrow S \vDash EXf$$ קיים מסלול $plot:$\pi = {S_0}{S_1}...$$ ממצב $plot:$S = {S_0}$$ כך שמתקיים $plot:${S_1} \vDash f$$ . נשים לב כי f היא נוסחת מצב. ב-CTL* הביטוי $plot:${S_1} \vDash f$$ היה מתפרש שונה.
$plot:$ \Leftrightarrow S \vDash E\left( {fUg} \right)$$ קיים מסלול $plot:$\pi = {S_0},{S_1},...$$ מ- כך שקיים $plot:$k \geqslant 0$$ כך ש- $plot:${S_k} \vDash g$$ ולכל $plot:${S_j} \vDash f\,\,\,\,\,\,\,\,\,0 \leqslant j < k$$ .
$plot:$ \Leftrightarrow S \vDash EGf$$ קיים מסלול $plot:$\pi $$ מ- כך שלכל $plot:$i \geqslant 0$$ $plot:${S_i} \vDash f$$

קיצורים:

$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}$$
$plot:$AF{f_1} \equiv \neg EG\neg {f_1}$$
$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)$$

המצבים עבורם $plot:${f_1}U{f_2}$$ לא מתקיים (אף פעם לא מתקיים $plot:${f_2}$$ , או שקיים מצב בו $plot:${f_1}$$ לא מתקיים לפני ש- $plot:${f_2}$$ התקיים)

דגשים:

נשים לב שבמקרה של 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} $$