# Introduction to Computational Logic

Student: B07902108 翁祖毅

### 1. $\phi U \psi \equiv \psi R(\phi \lor \psi) \land F \psi$

$\phi U \psi$
$\equiv \phi W\psi \land F \psi$
$\equiv \psi R(\phi \lor \psi) \land F \psi$

### 2. $\phi W \psi \equiv \psi R(\phi \lor \psi)$

Let $\pi$ be a path $s_0 \rightarrow s_1 \rightarrow$ ...

1. "only if" direction
* $\phi W \psi$
* Case 1: $\pi = \phi \rightarrow \phi \rightarrow$ ...
$\implies \psi R \phi \equiv \psi R (\phi \lor \psi)$
* Case 2: $\pi = \phi \rightarrow \phi \rightarrow$ ... $\rightarrow \psi$
$\implies \phi \lor \psi$ is always true and $\psi$ is true at some point
$\implies \psi R (\phi \lor \psi)$
2. "if" direction
* $\psi R(\phi \lor \psi)$
* $\pi = \phi \lor \psi \rightarrow$ ... $\rightarrow \phi \lor \psi$
* Case 1: $\psi$ is always false
$\implies \phi$ is always true
$\implies \phi W \psi$
* Case 2: $F \psi$
$\implies \phi W \psi$ (by definition)

### 3. $M,s \vDash AF(\phi \lor \psi)$ but $M \nvDash AF \phi \lor AF\psi$


### 4. Express the following statement in $CTL^∗$: “the event p is never true between the events q and r on a path.”

* $AG(q \implies \neg EF (p \land EFr)) \land AG(r \implies \neg EF (p \land EFq))$

### 5. $AGFp$ and $AGEFp$ specify different properties.


* $AGFp$: 每條路徑最終一定會到達右邊的 $p$。
* 假設有某條路徑永遠在 $\neg p$ 繞，就會不符合 $AGFp$ 的定義。