1.1 --- a/paper/src/paper.tex	Tue Jun 28 22:03:45 2011 +0200
     1.2 +++ b/paper/src/paper.tex	Wed Jun 29 00:11:59 2011 +0200
     1.3 @@ -36,6 +36,8 @@
     1.4  \newtheorem*{def:automata runs}{Runs}
     1.5  \newtheorem*{def:automata acceptance}{Acceptance}
     1.6  \newtheorem*{def:vocabulary}{Vocabulary}
     1.7 +\newtheorem*{def:models}{Models}
     1.8 +\newtheorem*{def:satisfiability}{Satisfiability}
     1.9  
    1.10  \theoremstyle{proposition}
    1.11  \newtheorem{prop:vocabulary sat}{Proposition}
    1.12 @@ -155,18 +157,21 @@
    1.13  \end{def:automata acceptance}
    1.14  
    1.15  \section{Linear temporal logic}
    1.16 -\subsection*{Sytnax}
    1.17 +\subsection{Sytnax}
    1.18  Let $\mathcal{P}$ be the countable set of \emph{atomic propositions}. The \emph{alphabet} of the language $L_{LTL}(\mathcal{P})$ is $\mathcal{P} \cup \{\neg, \lor, X, U\}$. We define the $L_{LTL}(\mathcal{P})$-\emph{formulae} $\varphi$ using following productions:
    1.19  \[\varphi ::= p \in \mathcal{P} \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, X \varphi \,|\, \varphi U \varphi\]
    1.20  
    1.21 -\subsection*{Interpretation}
    1.22 +\subsection{Interpretation}
    1.23  The intuition should go as follows: $\neg$ and $\lor$ correspond to the Boolean \emph{negation} and \emph{disjunction}, the unary temporal operator $X$ reads as \emph{next} and the binary temporal operator $U$ reads as \emph{until}.
    1.24  
    1.25  LTL is interpreted over \emph{computation paths}, where a computation corrensponds to a model over a \emph{Kripke-frame} constructed by the order of natural numbers.
    1.26  
    1.27 -\subsection*{Semantics}
    1.28 +\subsection{Semantics}
    1.29 +\begin{def:models}
    1.30  A \emph{model} is a function $\M: \N \to 2^\mathcal{P}$ over \emph{frame} $\mathcal{F}$. The frame constitutes a linear order over $\N$, which corresponds to the linear progression of time from the \emph{present/past} into the \emph{future}. Therefore $\M(i)$ assigns a set of \emph{positive atomic propositions} to each state of time instant $i$. Intuitively we say $p \in \mathcal{P}$ is \emph{true} at time instant $i$ iff $p \in \M(i)$.
    1.31 +\end{def:models}
    1.32  
    1.33 +\begin{def:satisfiability}
    1.34  A model $\M$ \emph{satisfies} an LTL-formula $\varphi$ at time instant $i$ is denoted by $\M,i \models \varphi$. Satisfiability of a formula $\varphi$ is defined inductively over the structure of $\varphi$:
    1.35  \begin{itemize}
    1.36  \item $\M,i \models p$ for $p \in \mathcal{P}$ iff $p \in \M(i)$
    1.37 @@ -175,7 +180,8 @@
    1.38  \item $\M,i \models X \varphi$ iff $\M,i+1 \models \varphi$
    1.39  \item $\M,i \models \varphi U \psi$ iff $\exists{k \geq i}: \M,k \models \psi$ and $\forall{i \leq j < k}: \M,j \models\varphi$
    1.40  \end{itemize}
    1.41 -%
    1.42 +\end{def:satisfiability}
    1.43 +
    1.44  \begin{def:vocabulary}
    1.45  Let $\varphi$ be a LTL-formula over atomic propositions $\mathcal{P}$, we define the \emph{vocabulary} $Voc(\varphi)$ of $\varphi$ inductively:
    1.46  \begin{multicols}{2}