Dont remember.
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}