# HG changeset patch
# User Eugen Sawin <sawine@me73.com>
# Date 1308784973 -7200
# Node ID 153633379524021d4c09612b095d3f5b08a08b87
# Parent  78929f746a5cc45ae1d6746af6555c2fa1d7c176
Dont remember.

diff -r 78929f746a5c -r 153633379524 paper/comments.txt
--- a/paper/comments.txt	Wed Jun 22 20:06:27 2011 +0200
+++ b/paper/comments.txt	Thu Jun 23 01:22:53 2011 +0200
@@ -7,7 +7,7 @@
 - no introduction to omega-regular languages
 - short introduction to LTL semantics
 - no automata complement construction
-
+- error on page 5: there must not be a state g in G along r
 
 
 graphs:
diff -r 78929f746a5c -r 153633379524 paper/src/paper.tex
--- a/paper/src/paper.tex	Wed Jun 22 20:06:27 2011 +0200
+++ b/paper/src/paper.tex	Thu Jun 23 01:22:53 2011 +0200
@@ -142,7 +142,7 @@
 \begin{def:automata acceptance}
 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$.
 
-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 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$.
 \end{def:automata acceptance}
 
 \section{Linear temporal logic}