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

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

6.3.3.2. הגדרה אינדוקטיבית של $plot:$ \vDash $$

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

סימונים בהגדרה:

$plot:${f_1},{f_2}$$ - נוסחאות מצב.
$plot:${g_1},{g_2}$$ - נוסחאות מסלול.

נוסחאות מצב:

$plot:$S \vDash p$$ עבור $plot:$p \in L\left( S \right) \Leftrightarrow p \in AP$$
$plot:$S\not \vDash f \Leftrightarrow S \vDash \neg f$$
$plot:$S \vDash {f_2} \Leftrightarrow S \vDash {f_1} \vee {f_2}$$ או $plot:$S \vDash {f_1}$$
$plot:$ \Leftrightarrow S \vDash E{g_1}$$ קיים מסלול $plot:$\pi $$ מ- כך ש- $plot:$\pi \vDash {g_1}$$

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

$plot:${S_0} \vDash f \Leftrightarrow \pi \vDash f$$ כאשר $plot:${S_0}$$ המצב הראשון ב- $plot:$\pi $$
$plot:$\pi \not \vDash {g_1} \Leftrightarrow \pi \vDash \neg {g_1}$$
$plot:$\pi \vDash {g_2} \Leftrightarrow \pi \vDash {g_1} \vee {g_2}$$ או $plot:$\pi \vDash {g_1}$$
$plot:${\pi ^1} \vDash {g_1} \Leftrightarrow \pi \vDash X{g_1}$$
$plot:$ \Leftrightarrow \pi \vDash {g_1}U{g_2}$$ קיים $plot:$k \geqslant 0$$ כך ש: $plot:${\pi ^k} \vDash {g_2}$$ , $plot:${\pi ^j} \vDash {g_1}$$ לכל $plot:$0 \leqslant j < k$$

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

$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$$

הארה

נסתכל על הקיצור האחרון $plot:$Gg \equiv \neg F\neg g$$ . האם היינו יכולים לכתוב אותו בעזרת Until?

כיוון אפשרי יכל להיות plot:$gUfalse$ אך זה איננו כיוון טוב – כי U מבטיח שבהכרח false יתקיים בסופו של דבר. האופרטור weak-until (הידוע גם בכינויו unless) היה יכול להתאים: plot:$gWfalse$ . אם weak-until היה חלק מהבסיס זו היתה הגדרה נכונה.