uni/sysver/ue3/assignment3_solution.tex

\documentclass[11pt,a4paper]{article} 
\usepackage{latexsym}
\usepackage{paralist}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{url}
\usepackage{tikz}
\usetikzlibrary{calc,intersections,angles,quotes}
\usepackage{stmaryrd}
\usepackage{float}
\let\origfigure\figure
\let\endorigfigure\endfigure
\renewenvironment{figure}[1][2] {
    \expandafter\origfigure\expandafter[H]
} {
    \endorigfigure
}

\newcommand\ctlA{\textsf{\textbf{A}}\,}
\newcommand\ctlE{\textsf{\textbf{E}}}
\newcommand\ltlF{\textsf{\textbf{F}}\,}
\newcommand\ltlG{\textsf{\textbf{G}}\,}
\newcommand\ltlU{\,\textsf{\textbf{U}}\,}
\newcommand\ltlX{\textsf{\textbf{X}}\,}
\newcommand\LTL[0]{$\mbox{\textsf{LTL}}$}

\parskip        0mm
\oddsidemargin  0in
\evensidemargin 0in
\textwidth      6in
\topmargin      0in
\marginparwidth 30pt
\textheight     9.2in
\headheight     .1in
\headsep        .1mm 

\title{VU Programm- und Systemverifikation\\ 
\Large Homework: Temporal Logic and Automated Reasoning}
\author{~}
\date{{\bf Due date:} May 27, 2021, \underline{1pm}}

\usepackage{listings}
\lstset{
  basicstyle=\footnotesize\ttfamily, % Standardschrift
  numbers=left,               % Ort der Zeilennummern
  numberstyle=\tiny,          % Stil der Zeilennummern
  numbersep=5pt,              % Abstand der Nummern zum Text
  tabsize=2,                  % Groesse von Tabs
  extendedchars=true,         %
  breaklines=true,            % Zeilen werden Umgebrochen
  keywordstyle=\ttfamily,
  stringstyle=\ttfamily, % Farbe der String
  showspaces=false,           % Leerzeichen anzeigen ?
  showtabs=false,             % Tabs anzeigen ?
  xleftmargin=17pt,
  framexleftmargin=17pt,
  framexrightmargin=5pt,
  framexbottommargin=4pt,
  showstringspaces=false      % Leerzeichen in Strings anzeigen ?        
}
\lstloadlanguages{ 
  C , C++, ml
}


\gdef\dash---{\thinspace---\hskip.16667em\relax}
\gdef\smdash--{\thinspace--\hskip.16667em\relax}
\newcommand{\emn}[1]{{\em #1\/}}
\gdef\op|{\,|\;}

\newcommand{\true}{{\sc true}}

\begin{document}

\maketitle

\paragraph{Task 1 (5 points):}

Consider the following Kripke Structure:

\begin{center}

\begin{tikzpicture}[>=latex,->,scale=0.7,label distance=-3mm,node distance=2cm]
            \tikzstyle{every node}=[draw,shape=circle,minimum size=9mm,font=\footnotesize];
            \tikzstyle{every path} = [draw,thick];
            \node (s0) [label=below:$s_0$] {$a$};
            \node[right of=s0]  (s1) [label=below:$s_1$] {$b$};
            \node[right of=s1]  (s2) [label=below:$s_2$] {$a$};
            \draw ($(s0)-(2cm,0)$)--(s0);
            \draw (s0) to (s1);
            \draw (s1) to (s2);
      %      \draw[loop above] (s0) to (s0);
            \draw[loop above] (s1) to (s1);
            \draw[loop above] (s2) to (s2);
\end{tikzpicture}

\end{center}

For each formula, give the
\underline{states of the Kripke structure for which the formula holds}. 
In other words, for each of the states from the set 
$\{s_0, s_1, s_2\}$,
consider the computation trees starting at that state, 
and for each tree, check whether the given formula holds on it or not.

\begin{enumerate}
\item $\ctlA \ltlF \ltlG a$

$\{s_2\}$
\vskip.5cm

\item $\ctlA\ltlF \ctlA\ltlG b$

$\emptyset$
\vskip.5cm

\item $\ctlA (a \wedge \ltlX b)$

$\{s_0\}$
\vskip.5cm

\item $\ctlA (b \ltlU a)$

$\{s_0, s_2\}$
\vskip.5cm

\item $\ctlA \ltlX \ltlX a$

$\{s_2\}$
\vskip.5cm

\item $\ctlA \ltlG \ltlF a$

$\{s_2\}$
\vskip.5cm

\item $\ctlA \ltlG \ltlF b$

$\emptyset$
\vskip.5cm

\item $\ctlE \ltlG \ltlF b$

$\{s_0, s_1\}$
\vskip.5cm

\item $\ctlA (a \ltlU b)$

$\{s_0, s_1\}$
\vskip.5cm

\item $\ctlE (b \ltlU a)$

$\{s_0, s_1, s_2\}$
\vskip1cm

\end{enumerate}

\clearpage

\paragraph{Task 2 (3 points):}

Consider the following Kripke Structure with initial state $s_0$:

\begin{center}

\begin{tikzpicture}[>=latex,->,scale=0.7,label distance=-3mm,node distance=2cm]
            \tikzstyle{every node}=[draw,shape=circle,minimum size=9mm,font=\footnotesize];
            \tikzstyle{every path} = [draw,thick];
            \node (s0) [label=below:$s_0$] {$a$};
            \node[right of=s0]  (s1) [label=below:$s_1$] {$b$};
            \node[right of=s1]  (s2) [label=below:$s_2$] {$a$};
            \draw ($(s0)-(2cm,0)$)--(s0);
            \draw (s0) to (s1);
            \draw (s1) to (s2);
      %      \draw[loop above] (s0) to (s0);
            \draw[loop above] (s1) to (s1);
            \draw[loop above] (s2) to (s2);
\end{tikzpicture}

\end{center}

\newcommand{\wedgi}{\;\wedge\; }

\begin{enumerate}

\vskip1cm

\item Does the LTL formula $\ctlA\ltlF\ltlG b$ hold in the initial
  state $s_0$?
  \begin{center}
  $\Box$ yes \qquad $\Box$ no 
\end{center} 
Justify your answer!

\begin{figure}
  \centering
  \includegraphics[scale=.6]{./res/2-1.png}
  \label{fig:justification-1}
\end{figure}
  
%  {s1, s2}
\item Does the CTL formula $\ctlA\ltlF\ctlE\ltlG b$ hold in the initial
  state $s_0$?
  \begin{center}
  $\Box$ yes \qquad $\Box$ no 
\end{center} 
Justify your answer!

\begin{figure}
  \centering
  \includegraphics[scale=.6]{./res/2-2.png}
  \label{fig:justification-2}
\end{figure}
 
\item Do the formulas (i) and (ii) above express the same property?
\begin{center}
  $\Box$ yes \qquad $\Box$ no 
\end{center} 
If not, explain why.

\begin{figure}
  \centering
  \includegraphics[scale=.6]{./res/2-3.png}
  \label{fig:justification-3}
\end{figure}
 
\end{enumerate}

\clearpage

\paragraph{Task 3 (2 points):}

Encode the following statements in temporal logic
(LTL if possible, CTL otherwise):

\begin{enumerate}
\vskip.5cm
\item Whenever the execution of a program encounters a
  {\em fault} it is possible to {\em recover} eventually.

\begin{figure}
  \centering
  \includegraphics[scale=.6]{./res/3-1.png}
  \label{fig:encoding-1}
\end{figure}
 
\item If an execution encounters {\em fault}s in three
  subsequent states, it will never {\em recover} again.

\begin{figure}
  \centering
  \includegraphics[scale=.6]{./res/3-2.png}
  \label{fig:encoding-2}
\end{figure}

 \item Whenever a state labeled with $a$ is reached, a state labeled
  with $b$ will be reached at a \emph{strictly later} point.

\begin{figure}
  \centering
  \includegraphics[scale=.6]{./res/3-3.png}
  \label{fig:encoding-3}
\end{figure}

\item All paths starting at the initial state lead to a
  cycle that does not contain a state labeled $a$.
 
\begin{figure}
  \centering
  \includegraphics[scale=.6]{./res/3-4.png}
  \label{fig:encoding-4}
\end{figure}
 
\end{enumerate}

\clearpage

\paragraph{Task 4 (5 points):}

Consider the following formula in propositional logic; is it satisfiable?
If yes, provide a satisfying assignment, if not,
\underline{give the reasoning that leads to this conclusion}.

\begin{multline}
  \overbrace{(x_{11} \vee x_{12})}^{C1} \wedgi
  \overbrace{(x_{21} \vee x_{22})}^{C2} \wedgi
  \overbrace{(x_{31} \vee x_{32})}^{C3}
  \wedgi \\
  \underbrace{(\neg x_{11} \vee \neg x_{21})}_{C4} \wedgi
  \underbrace{(\neg x_{11} \vee \neg x_{31})}_{C5} \wedgi 
  \overbrace{(\neg x_{12} \vee \neg x_{22})}^{C6} \wedgi
  \overbrace{(\neg x_{12} \vee \neg x_{32})}^{C7} \wedgi \\
  \underbrace{(\neg x_{21} \vee \neg x_{31})}_{C8} \wedgi 
  \underbrace{(\neg x_{22} \vee \neg x_{32})}_{C9}
\end{multline}

(The clauses in Formula (1) are labelled $C1$ to $C9$.)
\begin{itemize}
\item For each decision, provide the resulting implication/conflict graph!
\item For each conflict you reach, provide a corresponding learned clause!
\end{itemize}

\begin{figure}
  \centering
  \includegraphics[scale=.65]{./res/4-solution.png}
  \caption{implication/conflict graph and learnt clauses}
  \label{fig:implication-conflict-graph}
\end{figure}

\clearpage

\paragraph{Task 5 (3 points):}

\begin{enumerate}
\item Consider the following formulas in propositional logic; are they satisfiable? If
  yes, provide a satisfying assignment over booleans, if not, give
  the reasoning that leads to this conclusion.

\begin{figure}
  \centering
  \includegraphics[scale=.65]{./res/5-1.png}
  \label{fig:prop-logic}
\end{figure}

\item
  Consider the following formulas in Equality Logic; are they satisfiable? If
  yes, provide a satisfying assignment over integers, if not, give
  the reasoning based on equivalence classes that leads to this
  conclusion.

NOTE: I have done this exercise before I have learned about the merging of equivalence classes, but this particular "algorithm" is based on the same idea: reduce equivalent statements

\begin{equation}
  i = j \wedgi j = k \wedgi k = l \wedgi l \neq m \wedgi l \neq n \wedgi m = n \wedgi o \neq p \wedge o = q
\end{equation}

\begin{figure}
  \centering
  \includegraphics[scale=.65]{./res/5-2-1.png}
  \label{fig:eq-logic-1}
\end{figure}

\begin{equation}
  i = j \wedgi j = k \wedgi k = l \wedgi l \neq n \wedgi m = n \wedgi
  g(i) \neq g(m)
  \wedgi f(i) \neq f(l)
\end{equation}
 
\begin{figure}
  \centering
  \includegraphics[scale=.65]{./res/5-2-2.png}
  \label{fig:eq-logic-2}
\end{figure}

\vfill
\clearpage

\item
  Check the satisfiability of the following SMT formulas. 
  Assume that $x, y \in {\mathbb Z}$ are integer constants, and $f:
  {\mathbb Z} \rightarrow {\mathbb Z}$ and $g: {\mathbb Z} \times {\mathbb Z}
  \rightarrow {\mathbb Z}$ are unary and binary uninterpreted functions
  over integers respectively. 
  Whenever a formula is satisfiable, give a satisfying assignment for it, i.e.,
  integer values for all constants and function interpetations over integers
  that make the formula true under the assignment. 
  Whenever a formula is not satisfiable, give a reason why it is unsatisfiable.
  \begin{equation}
    g(3, y) = 5 \wedgi g(y, 3) = 4 \wedgi g(y, x) = g(x, y)
  \end{equation}
 
\begin{figure}
  \centering
  \includegraphics[scale=.65]{./res/5-3-1.png}
  \label{fig:smt-1}
\end{figure}
  
  \begin{multline}
    x = y \wedgi f(f(y)) = f(x) \wedgi f(1) \ne g(1, y) 
    \wedgi 1 = f(x) \wedgi g(1, x) = f(f(x))
  \end{multline}
\end{enumerate}

\begin{figure}
  \centering
  \includegraphics[scale=.65]{./res/5-3-2.png}
  \label{fig:smt-2}
\end{figure}
  
\vfill

\clearpage

\paragraph{Task 6 (2 points):}

\noindent
  Indicate whether the following statements are true or false!\\[2ex]

  \noindent
  \begin{tabular}{p{.65\textwidth}cc}
    {\bf Statement} & {\bf True} & {\bf False}\\[1ex]
    Any CTL formula starting with {\bf A} can be expressed in LTL
    & $\bigcirc$ & $\bigotimes$\\ 
    &&\\ 
    CTL$^{*}$ is the union of all CTL and LTL formulas. & $\bigcirc$ & $\bigotimes$\\ 
\vskip0.2cm
NOTE: consider ELTL
\vskip0.2cm
    &&\\
    Every CTL formula has an equivalent CTL formula containing only
    ${\bf AF}$, ${\bf EX}$, and ${\bf EU}$. & $\bigotimes$ & $\bigcirc$\\ % false
\vskip0.2cm
NOTE: $AF \varphi \mapsto \neg EG \neg \varphi$
\vskip0.2cm
    &&\\ 
    There is a non-empty Kripke structure~$K$ that satisfies
    $({\bf AG}\,{\bf AF} p) \wedge ({\bf EF}\,{\bf EG} \neg p)$. & $\bigcirc$ & $\bigotimes$\\
\vskip0.2cm
NOTE: $(AGAF p) \land (EFEG \neg p) = (\neg EF \neg(\neg EG \neg p)) \land (EFEG \neg p) = (\neg EFEG \neg p) \land (EFEG \neg p)$
  \end{tabular}
\vfill

Upload a pdf file with your solutions to TUWEL by May 27, 2021.

\end{document}