Notations

2 files changed, 35 insertions, 3 deletions

diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex
index d5de1a7..0149906 100644
--- a/Assignment1/assignment1.tex
+++ b/Assignment1/assignment1.tex
@@ -20,6 +20,9 @@
 	{\thmname{#1}\thmnumber{ #2}.\quad #3\\[4pt]}% Theorem head spec
 \theoremstyle{mydefinition}
 \newtheorem{xdefinition}{Definition}
+\newenvironment{definition}%
+	{\renewcommand{\qedsymbol}{$\blacksquare$}\pushQED{\qed}\begin{xdefinition}}%
+	{\popQED\end{xdefinition}}
 \newtheoremstyle{myexample}%
 	{2em}{2em}% Space above and below
 	{}% Body font
@@ -30,12 +33,13 @@
 	{\thmname{#1}\thmnumber{ #2}.\quad #3\\[4pt]}% Theorem head spec
 \theoremstyle{myexample}
 \newtheorem{xexample}{Example}
-\newenvironment{definition}%
-	{\renewcommand{\qedsymbol}{$\blacksquare$}\pushQED{\qed}\begin{xdefinition}}%
-	{\popQED\end{xdefinition}}
 \newenvironment{example}%
 	{\renewcommand{\qedsymbol}{$\blacksquare$}\pushQED{\qed}\begin{xexample}}%
 	{\popQED\end{xexample}}
+\newtheorem{xremark}{Remark}
+\newenvironment{remark}%
+	{\renewcommand{\qedsymbol}{$\blacksquare$}\pushQED{\qed}\begin{xremark}}%
+	{\popQED\end{xremark}}
 \usepackage{mathtools}
 \usepackage{mdframed}
 \usepackage{tikz}
@@ -43,6 +47,7 @@
 \usepackage{relsize}
 \usepackage{parskip}
 \usepackage{cleveref}
+\usepackage{stackengine}
 \crefname{figure}{Figure}{Figures}
 \usepackage[color]{changebar}
 \newif\ifchangebar\changebarfalse
@@ -319,8 +324,25 @@ $$
 	\end{matrix*}
 $$
 
+\subsubsection{Specifying Properties}
+% TODO Once operator
+
+\camil
+\begin{remark}[Other Notations]
+	% TODO: I don't find this place logical for this remark, but it is the same place as Remark 5.16 in the book.
+	Like for LTL, many different notations are used in literature for PLTL.
+	These include
+		$\mathbf X^{-1}, \mathbf G^{-1}, \mathbf F^{-1}$~\citep[e.g.]{Markey2003},
+		but also \raisebox{-1pt}{\tikz\draw[black,fill=black](0,0)circle(.4em);}$,\blacksquare,\blacklozenge$~\citep[e.g.]{Gabbay1989}
+		or $\stackinset{c}{}{c}{}{$\cdot$}{$\bigcirc$},\boxdot,\stackinset{c}{}{c}{}{$\cdot$}{$\lozenge$}$~\citep[e.g.]{Havelund2002}.
+	% It is always fun to come up with new versions and watch people struggling to reproduce them in \LaTeX.
+\end{remark}
+
+\erin
+\subsubsection{Equivalence of PLTL Formulae}
 Now that we have defined the formal semantics of PLTL,
 we can define equivalence on PLTL formulas.
+
 \begin{definition}[Equivalence of PLTL Formulae]
 	PLTL formulae $\phi_1,\phi_2$ are equivalent, denoted $\phi_1 \equiv \phi_2$ iff they verify the following property:
 	\[\text{for any path } \pi \text{ and any position } i, \pi \vDash_i \phi \Leftrightarrow \pi \vDash_i \psi \qedhere\]
@@ -352,6 +374,7 @@ Additionally, we can define another form of equivalence, initial equivalence:
 \section{Bibliographic Notes}
 % TODO: points to be added to 5.4
 % A possibly helpful list is at https://cstheory.stackexchange.com/a/29452
+% Also the bibliography file should be worked through.
 
 \section{Contribution}
 %TODO: Like we are some immature group of children, we have to provide proof of contribution
diff --git a/Assignment1/library.bib b/Assignment1/library.bib
index dc8247a..9a45e4a 100755
--- a/Assignment1/library.bib
+++ b/Assignment1/library.bib
@@ -66,5 +66,14 @@
 	author    = {Fiterau-Brostean, Paul and Lenaerts, Toon and Poll, Erik and De Ruiter, Joeri and Vaandrager, Frits and Verleg, Patrick},
 	title     = {Model Learning and Model Checking of SSH Implementations},
 	booktitle = {Proceedings 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, 13--14 July 2017, Santa Barbara, USA},
+	year      = 2017,
 	pages     = {142--151}
 }
+
+@inproceedings{Havelund2002,
+	author    = {Havelund, Klaus and Ro\c{s}u, Grigore},
+	title     = {Synthesizing Monitors for Safety Properties},
+	booktitle = {International Conference on Tools and Algorithms for the Contruction and Analysis of Systems, TACAS 2002},
+	year      = 2002,
+	pages     = {342--356}
+}