# HG changeset patch
# User Eugen Sawin <sawine@me73.com>
# Date 1309299119 -7200
# Node ID ebda6a5fc738d547123ee1ca8548362feba7d0e3
# Parent  9e5a3c5efff7806e2f5fa38dfa2dcab64d3858f6
Nothing.

diff -r 9e5a3c5efff7 -r ebda6a5fc738 paper/src/paper.tex
--- a/paper/src/paper.tex	Tue Jun 28 22:03:45 2011 +0200
+++ b/paper/src/paper.tex	Wed Jun 29 00:11:59 2011 +0200
@@ -36,6 +36,8 @@
 \newtheorem*{def:automata runs}{Runs}
 \newtheorem*{def:automata acceptance}{Acceptance}
 \newtheorem*{def:vocabulary}{Vocabulary}
+\newtheorem*{def:models}{Models}
+\newtheorem*{def:satisfiability}{Satisfiability}
 
 \theoremstyle{proposition}
 \newtheorem{prop:vocabulary sat}{Proposition}
@@ -155,18 +157,21 @@
 \end{def:automata acceptance}
 
 \section{Linear temporal logic}
-\subsection*{Sytnax}
+\subsection{Sytnax}
 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:
 \[\varphi ::= p \in \mathcal{P} \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, X \varphi \,|\, \varphi U \varphi\]
 
-\subsection*{Interpretation}
+\subsection{Interpretation}
 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}.
 
 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.
 
-\subsection*{Semantics}
+\subsection{Semantics}
+\begin{def:models}
 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)$.
+\end{def:models}
 
+\begin{def:satisfiability}
 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$:
 \begin{itemize}
 \item $\M,i \models p$ for $p \in \mathcal{P}$ iff $p \in \M(i)$
@@ -175,7 +180,8 @@
 \item $\M,i \models X \varphi$ iff $\M,i+1 \models \varphi$
 \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$
 \end{itemize}
-%
+\end{def:satisfiability}
+
 \begin{def:vocabulary}
 Let $\varphi$ be a LTL-formula over atomic propositions $\mathcal{P}$, we define the \emph{vocabulary} $Voc(\varphi)$ of $\varphi$ inductively:
 \begin{multicols}{2}