llerbs/klausuren-allgemein
1
0
Fork 0
forked from klausuren/klausuren-allgemein
Code Issues Pull Requests Releases Wiki Activity

Falscher Ordner

Browse Source
This commit is contained in:
Karp 2015-11-12 14:50:27 +01:00
parent 630bfdd12b
commit 3742fcea29
1 changed files with 0 additions and 78 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

78
logik_sav_ss15.tex
View File

@ -1,78 +0,0 @@
\include{settings}
\usepackage{enumitem}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{graphicx}
\begin{document}
\klausur{Logik (Specification and Verification)}{Prof. M. Mendler}{Sommersemester 15}{90}{Wörterbuch}
\textbf{Basic Modal Logic}
\begin{enumerate}
\item What are the main difference between First-order Predicate Logic and Propositional Modal Logic? \\
$\left[Punkte: 5\right]$
\item For this exercise we fix the signature \textit{I = \{marriedTo, likes, loves\}} with (propositional) variables \textit{Var = \{Doctor, Male\}}.
\begin{enumerate}[label=(\alph*)]
\item The picture below defines a particular Kripke model \textit{$\mathcal{M} = \{\mathcal{F}, V\}$} for our signatur \textit{(I, Var)}. The Frame \textit{$\mathcal{F} = (W, \underrightarrow{i} \mid i \in I)$} has worlds \textit{W = \{b, m, d, c, a, e\}} and the accessability relations \textit{$\underrightarrow{i}$} for \textit{$i \in I$} as seen in the picture. The valuation is such that \textit{V(Male) = \{m, d, e\}} and \textit{V(Doctor) = \{a, b, c, d\}}:\\
\begin{figure}[h]
\centering
\includegraphics[scale=0.8]{Graph_2a.png}
\end{figure}
Consider the modal formula
\textit{$\Phi := <likes>(Doctor \wedge <loves>(Male \wedge [loves]\neg Doctor))$} \\
Which individuals (worlds) satisfy this formula, i. e., for which \textit{w $\in$ W} do we have \textit{$\mathcal{M}, w \models \Phi$}? Justify your answer! \\
$\left[Punkte: 15\right]$
\item Find two modal formulas $\Phi_{a}$, $\Phi_{b}$ which separate the individuals (worlds) a and b, i. e., each satisfies one of the formulas but not the other. More precisely, construct $\Phi_{a}$, $\Phi_{b}$ such that \textit{$\mathcal{M}, a \models \Phi_{a} \wedge \neq \Phi_{b}$} and \textit{$\mathcal{M}, b \models \Phi_{b} \wedge \neg \Phi_{a}$}. Explain your workings! \\
$\left[Punkte: 15\right]$
\item Consider the extended modal signatur \textit{(I, Var')} where we have added a new propositional variable Female, i. e., \textit{$Var' = Var \cup \{Female\}$}. Define a valuation \textit{$V'(Female) \subseteq W$} for the new variable so that the formula\\
\noindent\hspace*{10mm} \textit{$\psi = (Male \vee Female) \wedge \neg(Male \wedge Female) \wedge (Male \supset [marriedTo] Female)$} \\
is valid in \textit{$\mathcal{M}' = (\mathcal{F}, V')$}. Take the same frame $\mathcal{F}$ as in the previous question parts and let \textit{V'(Male) = V(Male)}. Justify your workings!\\
$\left[Punkte: 10\right]$
\end{enumerate}
\newpage
\textbf{PLTL}
\item
\begin{enumerate}[label=(\alph*)]
\item Give a formal (or otherwise precise) definition of the semantics of the \glqq strong until\grqq\ operator $\Phi_{a} \cup \Phi_{b}$ in PLTL. \\
$\left[Punkte: 10\right]$
\item What is weak fairness and what is strong fairness? Illustrate the difference using one or more examples of your own choice.\\
$\left[Punkte: 5\right]$
\item The Simple Mail Transfer Protocol (SMTP) is used by a mail client to transmit email to a mail server on the internet. As seen in the picture the SMTP protocol typically proceeds in three phases. The first phase is the opening phase (OPEN) in which the client establishes a connection with the server and transmits the sender and receiver addresses. The second ohase is the data transmission phase (DATA) in which the server specifies how the email data are to be terminated (here, for instance, by the sequence <CR><LF>.<CR><LF>) and in which the client transmits the actual contents of the email. In the third and final phase (CLOSE) the client terminates the connection.\\
Consider OPEN, DATA, CLOSE as atomic predicates (propositional variables) which describe the state of the global system consisting of client and server together, specifying that the global system is in phase OPEN, DATA, CLOSE, respectively.\\
Find a PLTL formula which states \\
\noindent\hspace*{10mm}\glqq Between every OPEN and CLOSE there must lie a DATA phase.\grqq\ \\
Hint: Think about the bad case and exclude it! \\
$\left[Punkte: 15\right]$
\end{enumerate}
\newpage
\textbf{The Logic of Knowledge (S5)}
\item
\begin{enumerate}[label=(\alph*)]
\item Recall the following famous axiom schemes \\
\noindent\hspace*{20mm} K:\noindent\hspace*{8mm} $\square(P \supset Q) \supset (\square P \subset \square Q)$ \\
\noindent\hspace*{20mm} T:\noindent\hspace*{8mm} $\square P \subset P$ \\
\noindent\hspace*{20mm} D:\noindent\hspace*{8mm} $\square P \subset \diamond P$ \\
\noindent\hspace*{20mm} B:\noindent\hspace*{8mm} $P \subset \square \diamond P$ \\
\noindent\hspace*{20mm} 4:\noindent\hspace*{8mm} $\square P \subset \square \square P$ \\
\noindent\hspace*{20mm} 5:\noindent\hspace*{8mm} $\diamond P \subset \square \diamond P$ \\
that play an important role in the axiomatisation of modal logics. \\
Which if these axiom schemes are valid in the modal system S5 used to formalise knowledge?\\
$\left[Punkte: 5\right]$
\item Using S5 tableau calculus (see appendix) show that S5; ; $\models \Phi$ where \\
\noindent\hspace*{20mm} $\Phi = \neg \diamond(P \vee \square Q) \vee (\square \diamond P \vee \square Q)$ \\
i. e., show that $\Phi$ is valid in all S5-Frames. Make sure you explain why this follows from your workings! \\
Note that negation and the modal opreators have highest binding power, so that for instance, $\square \diamond P \vee \square Q$ is the same as $(\square(\diamond P)) \vee (\square Q)$ and $\neg \diamond(P \vee \square Q) \vee (\psi \vee \theta)$ is the same as $(\neg (\diamond (P \vee (\square Q)))) \vee (\psi \vee \theta)$. \\
$\left[Punkte: 10\right]$
\end{enumerate}
\end{enumerate}
\end{document}