diff options
author | Camil Staps | 2018-04-17 11:07:20 +0200 |
---|---|---|
committer | Camil Staps | 2018-04-17 11:07:20 +0200 |
commit | 64c60cf71492ae3c40d2c4cbe11a650d32ced19d (patch) | |
tree | 9a38efaebfb4396511998bb4839e7f6f94340c2f /Assignment1/exercises.tex | |
parent | Start 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.tex | 25 |
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$, \[ |