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

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

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

6.3.6. זיהוי ביטויים מהלוגיקות השונות

  • CTL – הביטויים בלוגיקה זו מורכבים תמיד מזוגות – כמת+אופרטור.
  • LTL – ביטויים בלוגיקה זו מתחילים תמיד בכמת A, ולאחריו במהלך הביטוי אין כמתים נוספים.
  • CTL* – הביטויים מתחילים בכמת ולאחריו אין הגבלות כלשהן. לחילופין הביטוי הוא מצב.

משפט (ללא הוכחה):

  • ל-plot:$LTL$ ו-plot:$CTL$ כוח ביטוי בלתי ניתן להשוואה. בכל אחת מהן יש נוסחה שאין לה נוסחה שקולה בלוגיקה השניה.
  • CTL* הינה בעלת כוח ביטוי גדול ממש גם מ-plot:$CTL$ וגם מ-plot:$LTL$.



דוגמא נוספת להבדל בין CTL ל-LTL:

נראה כי plot:$AFAGp \in CTL$ איננה שקולה לנוסחה plot:$AFGp \in LTL$.

plot:$AFAGp$  אומרת: קיימת נקודה בגרף החל ממנה plot:$AGp$.

plot:$AFGp$ אומרת: בכל המסלולים בגרף, קיימת נקודה החל ממנה מתקיים plot:$p$.

כדי להראות שהנוסחאות אינן שקולות יש להראות מבנה המספק אחת אך אינו מספק את השניה:

המבנה מספק את plot:$AFGp$ אך אינו מספק את plot:$AFAGp$. המסלול הבעייתי הוא מסלול בו נלך על 1 אינסוף פעמים – אין סיפא שממנה והלאה plot:$p$ יתקיים.

משפט (ללא הוכחה):

בהנתן נוסחת CTL plot:$p$, אם קיימת ב-LTL נוסחה plot:$q$ השקולה ל-plot:$p$, נקבלה על ידי מחיקת כל הכמתים מ-plot:$p$, והוספת A בתחילת הביטוי שנוצר.



תגיות המסמך:

לפרק הקודם6.3.5. LTL
לפרק הבא6.4. אלגוריתם מפורש לבדיקת מודל CTL
אין תגובות!
שיתוף:
| עוד