1 files changed, 46 insertions, 0 deletions
diff --git a/assignment2.tex b/assignment2.tex
new file mode 100644
index 0000000..0b82ded
--- /dev/null
+++ b/assignment2.tex
@@ -0,0 +1,46 @@
+\documentclass[a4paper]{article}
+
+\usepackage{geometry}
+\usepackage[english]{babel}
+
+\usepackage{enumitem}
+\setenumerate[1]{label=\alph*)}
+
+\usepackage{fancyhdr}
+\renewcommand{\headrulewidth}{0pt}
+\renewcommand{\footrulewidth}{0pt}
+\fancyhead{}
+\fancyfoot[C]{Copyright {\textcopyright} 2016 Camil Staps}
+\pagestyle{fancy}
+
+\usepackage{sv}
+
+\title{Software Verification - assignment 2}
+\author{Camil Staps}
+
+\def\run#1{\mathit{run}_{#1}}
+\def\stop#1{\mathit{stop}_{#1}}
+
+\begin{document}
+
+\maketitle
+\thispagestyle{fancy}
+
+\setcounter{section}{2}
+\section{CTL-properties of processes}
+
+\begin{enumerate}
+    \item $\invariantly(\lnot(\run1\land\run2))$.
+    \item $\potentially(\run1\land\run2)$.
+    \item $\inevitably\eventually(\run1)$.
+    \item $\potentially\eventually(\run1)$.
+    \item $(\potentially(\lnot\run1\until\run2)) \land (\potentially(\lnot\run2\until\run1))$.
+    \item Impossible: `never' cannot be expressed in CTL: does it mean `in no case whatsoever can this happen' or `there is a path for which this never happens'? But in LTL: $(\always\lnot\run2)\then(\always\run1)$.
+    \item For the same reason as above we cannot express this in CTL. We cannot express this in LTL either, because `may \dots forever' can only be expressed in CTL.
+    \item $\invariantly\exists\next\stop{i}$ with $i\in\{1,2\}$.
+    \item $\invariantly((\forall\lnot\stop1)\then\inevitably\run1)$.
+    \item $\invariantly(\lnot\run1\then\potentially(\lnot\run1\untilW\run2))$.
+\end{enumerate}
+
+\end{document}
+