Add definitions of wff, wff0, wff+, wff- (and an exercise about them)

1 files changed, 25 insertions, 0 deletions

diff --git a/Assignment1/exercises.tex b/Assignment1/exercises.tex
index 371dc0f..9126427 100644
--- a/Assignment1/exercises.tex
+++ b/Assignment1/exercises.tex
@@ -8,6 +8,31 @@
 
 \camil
 \begin{exercise}
+	For the PLTL formulas over $AP=\{a,b\}$ given below, determine whether they are \wffn, \wffp, \wfff\ or neither.
+
+	\begin{multicols}{2}
+		\begin{enumerate}[label=(\alph*)]
+			\item $\Xop a$.
+			\item $a \Sop b$.
+			\item $(\lnot (a \land b)) \land (\lnot (\lnot a \land \lnot b))$.
+			\item $a \Uop a$.
+			\item $a \land ((b \Uop a) \lor \lnot(b \Uop a))$.
+			\item $\text{false} \rightarrow (a \Uop b)$.
+		\end{enumerate}
+	\end{multicols}
+
+	\begin{answer}
+		(a) \wfff;
+		(b) \wffp;
+		(c) \wffn;
+		(d) \wfff;
+		(e) neither;
+		(f) neither.
+		Note that the definition of the classes is syntactic, not semantic.
+	\end{answer}
+\end{exercise}
+
+\begin{exercise}
 	On page~\pageref{pltl:dual-modalities}, we discussed informally why the dual modalities $\lozenge^{-1}\square^{-1}\phi$ and $\square^{-1}\lozenge^{-1}\phi$ are both equivalent to \enquote{at the first moment in time, $\phi$}.
 	Prove this formally, i.e.\ that for all infinite words $\sigma$ and $i\in\mathbb N$,
 	\[