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

6.3. לוגיקות טמפורליות פסוקיות

נציג כעת מספר לוגיקות טמפורליות פסוקיות שונות בהן נשתמש לבדיקת מודל, והן:

• הלוגיקה CTL (Computation Tree Logic)
• הלוגיקה LTL (Linear Temporal Logic)
• הלוגיקה CTL*.

הלוגיקה CTL* היא הגדולה מבין 3 הלוגיקות והיא מכילה ממש את הלוגיקות CTL ו-LTL.

הלוגיקות CTL ו-LTL הן בעלות יכולת ביטוי שאינה ניתנת להשוואה. הלוגיקות נבדלות בשילובים של כמתי מסלול ואופרטורים טמפורליים המותרים בכל אחת מהן. נציג את הלוגיקות השונות ונעמוד על ההבדלים ביניהן.

מבחינה היסטורית, אמיר פנואלי הציע ב-1977 לעשות שימוש ב-LTL לצורך הוכחת תוכניות. 4 שנים מאוחר יותר, ב-1981 המציאו Clarke ו-Emerson את CTL ואת בדיקת המודל באמצעות CTL. הלוגיקה CTL* הומצאה רק מאוחר יותר, ב-1986. בפרקטיקה LTL ו-CTL נמצאים בשימוש בפועל, ואילו CTL* נפוצה הרבה פחות. הסיבה העיקרית היא כוחות שוק המקדמים לוגיקות אלו.