|
|
@ -1,12 +1,12 @@ |
|
|
|
We use the following Boolean variables: |
|
|
|
\begin{itemize} |
|
|
|
\item $a$ represents ``The robot visits region A'' |
|
|
|
\item $b$ represents ``The robot visits region B'' |
|
|
|
\item $c$ represents ``The robot visits region C'' |
|
|
|
\item $b$ represents ``The robot visits region B'' |
|
|
|
\item $c$ represents ``The robot visits region C'' |
|
|
|
\end{itemize} |
|
|
|
|
|
|
|
\begin{itemize} |
|
|
|
\item $\varphi_1 \coloneqq E(GF a \wedge GF c)$ |
|
|
|
\item $\varphi_2 \coloneqq A (GF a \wedge FG \neg c)$ |
|
|
|
\item $\varphi_3 \coloneqq A (GF a \rightarrow GF c)$ |
|
|
|
\end{itemize} |
|
|
|
\item $\varphi_1 \coloneqq E(GF a \land GF c)$ |
|
|
|
\item $\varphi_2 \coloneqq A (GF a \land GF c)$ |
|
|
|
\item $\varphi_3 \coloneqq A (GF a \imp FG \neg c)$ |
|
|
|
\end{itemize} |