7.4.1. CTL*
CTL* הינה סוג של לוגיקה טמפורלית, המוגדרת באמצעות 2
סוגי נוסחאות:
- נוסחאות מצב שמתפשרות במצב נתון.
- נוסחאות מסלול שמתפרשות במסלול נתון.
הגדרה אינדוקטיבית של הלוגיקה:
נוסחאות מצב
- בסיס: נוסחאות אטומיות
.
- כללי יצירה:
- אם
נוסחאות מצב אז
הן נוסחאות מצב.
- אם
נוסחת מסלול אז
היא נוסחת מצב.
נוסחאות מסלול
- בסיס: כל נוסחת מצב היא נוסחת מסלול.
(הנוסחה תבחן על המצב הראשון במסלול).
- כללי יצירה: אם
נוסחאות מסלול אז
הן נוסחאות מסלול.
CTL* היא קבוצת נוסחאות המצב המוגדרות לפי
הגדרה זו.
קיצורים:
(אופרטורים המוגדרים בעזרת האופרטורים הבסיסיים)