ECE 479: Formal Verification

Temporal Logic

Example 1

Lets look that an example and see if it satisfies $EG(a \rightarrow b)$ which means $EG(\neg a \vee b)$.

First, we can go through and mark all unspecified states as $\neg a$ like:

So the first path doesn't work but the second path does satisfy the condition so the condition is true.

Example 2

$EG[a \rightarrow Axr]$ which means if $a$ is true, the from that state, for all paths, next time R needs to be true.

So first, we can see that one of the paths doesn't have any states with $a$ so by default, it satisfies our condition.

Now, we will look at the top path. This does not satisfy as the next time state after $a$ doesn't have $r$ equals true.

Finally, if we look at the left-most path, we see that when there is an $a$, each of the next time states has $r$ equals to true. Therefore, it satisfies the formula.

And because this tree has two paths that satisfy the condition, the tree will satisfy the condition.

Example 3

$EFa \rightarrow bUc$

So once $a$ becomes true, then, for this formula to be satisfied, $c$ has to be true, with every preceding state having to have $b$ as true.

So this example satisfies this condition.

State Properties vs Path Properties

$a$, $c$, $e$: State Properties
$Ga$, $G \neg a \vee b$: Path Properties
$Axa$, $EG$, $EF$, $AaRb$, $EaUb$: State Properties

State properties have to hold in a state.

Path properties have to hold along a path.

$Eg[a \rightarrow Axr$

If $f$ and $g$ are state properties, then $\neg f$, $f \vee g$, and $f \wedge g$ are also state properties.

Natural Language to Temporal Logic

Example 1

It is possible to get to a state where $Start$ holds but $Ready$ doesn't hold.

So $Start$ ($s$) and $Ready$ ($r$) are atomic properties.

$x : s \wedge \neg r$

What CTL operators describes this situation?

Because it is not saying that all paths have to hold, we should use $E$.

So the CTL representation of this statement is $EF[s \wedge \neg r]$