ECE 479: Formal Verification

CTL*

1. Boolean Operators
2. Path Quantifiers: $A$ - For all paths : $E$ - There exists a path
3. Temporal Operators

Temporal Operators:

• $x$: Next Time: Requires the property to hold in the second state of the path.
• $G$: Global: Requires that the property holds in every state of the path.
• $F$: Future: Requires that the property holds somewhere on the subsequent path.
• $U$: Until: Combines two properties. Holds true if there is a state on the path where the second property holds and at every preceding state on the path, the first property holds.
• $R$: Release: Holds when each preceding state holds true until and including the first position in which the second property holds.

Example

Now we start checking the paths:
$xb$? This means next time $b$. This is satisfied, so we use the symbol $\vDash$
$Axb$? This means that all paths have a next time of $b$. This is not satisfied, so we use the symbol $\nvDash$

So for this example, we can say:
$xb \vDash P_1$
$xb \nvDash P_2$
Therefore
$Axb \nvDash t_1$

What about $Exb$?
This is asking does a path exist where the next time $b$ is true.
$Exb \vDash t_1$

Now we continue and keep finding what is satisfied.
$Axa \vDash t_1$
$Exa \vDash t_1$