1.1 --- a/paper/comments.txt	Wed Jun 22 20:06:27 2011 +0200
     1.2 +++ b/paper/comments.txt	Thu Jun 23 01:22:53 2011 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  - no introduction to omega-regular languages
     1.5  - short introduction to LTL semantics
     1.6  - no automata complement construction
     1.7 -
     1.8 +- error on page 5: there must not be a state g in G along r
     1.9  
    1.10  
    1.11  graphs:

     2.1 --- a/paper/src/paper.tex	Wed Jun 22 20:06:27 2011 +0200
     2.2 +++ b/paper/src/paper.tex	Thu Jun 23 01:22:53 2011 +0200
     2.3 @@ -142,7 +142,7 @@
     2.4  \begin{def:automata acceptance}
     2.5  Let $A = (\Sigma, S, S_0, \Delta, F)$ be an automaton and let $\rho$ be a run of $A$, we define $inf(\rho) = \{s \in S \mid \exists^\omega{n \in \mathbb{N}_0}: \rho(n) = s\}$, where $\exists^\omega$ denotes the existential quantifier for infinitely many occurances, i.e., $s$ occurs infinitely often in $\rho$.
     2.6  
     2.7 -The run $\rho$ is \emph{accepting}, iff $inf(\rho) \cap F \neq \emptyset$, i.e., there exists an \emph{accepting state} which occurs infinitely often in the run $\rho$. The automaton $A$ \emph{accepts} an input word $w$, iff there exists a run $\rho$ of $A$ on $w$, such that $\rho$ is \emph{accepting}.
     2.8 +The run $\rho$ is \emph{accepting}, iff $inf(\rho) \cap F \neq \emptyset$, i.e., there exists an \emph{accepting state} which occurs infinitely often in the run $\rho$. The automaton $A$ \emph{accepts} an input word $w$, iff there exists a run $\rho$ of $A$ on $w$, such that $\rho$ is \emph{accepting}. The language $L_\omega(A)$ recognised by automaton $A$ is the set of all infinite words accepted by $A$.
     2.9  \end{def:automata acceptance}
    2.10  
    2.11  \section{Linear temporal logic}