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

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

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

6.3.1. מרכיבי הלוגיקות הטמפורליות

קבוצת נוסחאות אטומיות: plot:$AP$ סופית

אופרטורים בוליאניים:  plot:$ \wedge , \vee ,\neg ,...$

אופרטורים טמפורליים:

  • plot:$Fp$ (Future, Eventually) – קיים מצב בעתיד שבוplot:$p$ מתקיים. (החלטה: העתיד כולל גם את הצומת הנוכחי, "ההווה").
  • plot:$Gp$ (Globally) - plot:$p$ מתקיים בכל מצב על המסלול (החל מהצומת הנוכחי).
  • plot:$Xp$ (next) - plot:$p$ נכון במצב הבא בסדרה. (המצב השני בסדרה)
  • plot:$pUq$ (Until) - plot:$q$ מתקיים מתישהו בעתיד ו-plot:$p$ נכון בכל המצבים הקודמים.

כמתי מסלול: 

  • plot:$A\varphi $ - plot:$\varphi $ מתקיים על כל המסלולים, כולל המצב הנוכחי.
  • plot:$E\varphi $ - קיים לפחות מסלול אחד היוצא מהמצב הנוכחי עבורו plot:$\varphi $ מתקיים.


תגיות המסמך:

לפרק הקודם6.3. לוגיקות טמפורליות פסוקיות
לפרק הבא6.3.2. אופרטורים טמפורליים
אין תגובות!
שיתוף:
| עוד