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

7.4.4. הגדרת האופרטורים הטמפורלים – ויקיפדיה האנגלית

The temporal operators are the following:

• Quantifiers over paths
• A φ - All: φ has to hold on all paths starting from the current state.
• E φ - Exists: there exists at least one path starting from the current state where φ holds.
• Path-specific quantifiers
• X φ - Next: φ has to hold at the next state (this operator is sometimes noted N instead of X).
• G φ - Globally: φ has to hold on the entire subsequent path.
• F φ - Finally: φ eventually has to hold (somewhere on the subsequent path).
• φ U ψ - Until: φ has to hold until at some position ψ holds. This implies that ψ will be verified in the future.
• φ W ψ - Weak until: φ has to hold until ψ holds. The difference with U is that there is no guarantee that ψ will ever be verified. The W operator is sometimes called "unless".

In CTL*, the temporal operators can be freely mixed. In CTL, the operator must always be grouped in two: one path operator followed by a state operator.