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

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

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

6.4.4.2. סמנטיקה

הגדרת ספיקות של נוסחאות plot:$CT{L^F}$ נעשית מעל מבנה קריפקה הוגן plot:$M,S{ \vDash _F}\varphi $

הסמנטיקה זהה ל-plot:$ \vDash $, למעט כמתי מסלולים:

  • plot:$ \Leftrightarrow S{ \vDash _F}EX{\varphi _1}$ קיים מסלול הוגן היוצא מ-plot:$S$ כך ש- plot:${S_1}{ \vDash _F}{\varphi _1}$
  • plot:$ \Leftrightarrow S{ \vDash _F}AX{\varphi _1}$ לכל חישוב הוגן היוצא מ-plot:$S$ כך ש- plot:${S_1}{ \vDash _F}{\varphi _1}$
  • plot:$ \Leftrightarrow S{ \vDash _F}E\left( {{\varphi _1}U{\varphi _2}} \right)$ קיים מסלול הוגן plot:$\pi $ וכן קיים plot:$k \geqslant 0$ כך שמתקיים plot:${\pi ^k} \vDash {\varphi _2}$ וכןplot:${\pi ^j} \vDash {\varphi _1}$ לכל plot:$0 \leqslant j < k$
  • plot:$ \Leftrightarrow S{ \vDash _F}A\left( {{\varphi _1}U{\varphi _2}} \right)$ לכל מסלול הוגן plot:$\pi $ קיים plot:$k \geqslant 0$ כך שמתקיים plot:${\pi ^k} \vDash {\varphi _2}$ וכן plot:${\pi ^j} \vDash {\varphi _1}$ לכל plot:$0 \leqslant j < k$

נסמן plot:${A_F}\varphi \,\,, & \,\,{E_F}\varphi $ כשנרצה להגיד כי "קיים מסלול הוגן" או כאשר "כל המסלולים ההוגנים היוצאים מהמצב ...".

יתכן שממצבplot:$S$ אין אף מסלול הוגן ואז:

  • plot:$S{ \vDash _F}A\varphi $ לכלplot:$\varphi $
  • plot:$S{\not  \vDash _F}E\varphi $ לכלplot:$\varphi $



תגיות המסמך:

לפרק הקודם6.4.4.1. הגדרות ודוגמאות ראשונות
לפרק הבא6.4.4.3. אלגוריתם לחישוב קבוצת המצבים המספקים plot:${E_F}G{\varphi _1}$
אין תגובות!
שיתוף:
| עוד