summaryrefslogtreecommitdiff
path: root/Assignment1/exercises.tex
diff options
context:
space:
mode:
authorCamil Staps2018-04-17 11:07:20 +0200
committerCamil Staps2018-04-17 11:07:20 +0200
commit64c60cf71492ae3c40d2c4cbe11a650d32ced19d (patch)
tree9a38efaebfb4396511998bb4839e7f6f94340c2f /Assignment1/exercises.tex
parentStart of semantic algorithm (diff)
Add definitions of wff, wff0, wff+, wff- (and an exercise about them)
Diffstat (limited to 'Assignment1/exercises.tex')
-rw-r--r--Assignment1/exercises.tex25
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$,
\[