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

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

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

6.3.5. LTL

לוגיקה עיתית ליניארית Linear temporal logic: נוסחאות LTL הן מהצורה plot:$Af$ כאשרplot:$f$ נוסחת מסלול שבה נוסחאות המצב הן נוסחאות אטומיות בלבד. (אין כמתי מסלול ב-LTL מלבד

ה-plot:$A$החיצוני).

נוסחת מסלול LTL היא מהצורה:

  • plot:$p \in AP$
  • אם plot:$f,g$ נוסחאות מסלול LTL, אז גם plot:$\neg f,fUg,Xf,f \vee g$ הן נוסחאות מסלול LTL.

נוסחת LTL היא מהצורה plot:$Af$ כאשר plot:$f$ היא נוסחת מסלול LTL.

דוגמאות לנוסחאות מסלול LTL: plot:$GFp,FGp,\left( {Fb} \right)Ua$.

Linear Time Logic                                      Branching Time Logic     

יש הבדל בין שתי צורות הבדיקה (הימנית לעומת שתי השמאליות): בצורה הימנית בנקודה plot:${p_2}$ עוד לא נעשתה ההחלטה לאן לנוע ואילו בצורות השמאליות ההחלטה כבר התקבלה.

  • ב-CTL יש אפשרות בחירה בעתיד.
  • ב-LTL אין אפשרות בחירה בעתיד.


דוגמא

נראה את ההבדל בין CTL ל-LTL על ידי דוגמא. נביט בביטוי ה-CTL הבא: plot:$AFAXp$.

איך יראה המבנה המתאים לביטוי זה? המבנה יהיה מהצורה:

במבנה מסלולים באורכים שונים, ובכל מסלול שכזה קיים מצב שבו כל הבנים מספקים p.

הלוגיקה LTL לא מאפשרת לנו לבטא מבנה כזה. נוסחה קרובה ב-LTL הינה plot:$AFXp$. הנוסחה אומרת כי בכל מסלול במבנה, נגיע למצב שבו המצב הבא מספק את plot:$p$. עם זאת, אנחנו לא יכולים להבטיח ש-plot:$p$ יסתפק על כל הבנים של מצב כלשהו בהמשך.

תגיות המסמך:

לפרק הקודם6.3.4. CTL
לפרק הבא6.3.6. זיהוי ביטויים מהלוגיקות השונות
אין תגובות!
שיתוף:
| עוד