assignment2.tex


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
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}