1.1 --- a/paper/src/paper.tex Wed Jun 29 00:11:59 2011 +0200
1.2 +++ b/paper/src/paper.tex Wed Jun 29 18:39:07 2011 +0200
1.3 @@ -7,18 +7,24 @@
1.4 \usepackage{algorithmic}
1.5 \usepackage{multicol}
1.6 %\usepackage{fullpage}
1.7 +%\usepackage{a4wide}
1.8 +\usepackage[left=3.9cm, right=3.9cm]{geometry}
1.9 %\usepackage[T1]{fontenc}
1.10 %\usepackage{arev}
1.11 %\pagestyle{headings}
1.12 +
1.13 \renewcommand{\familydefault}{\sfdefault}
1.14 \newcommand{\M}{\mathcal{M}}
1.15 \newcommand{\N}{\mathbb{N}_0}
1.16 +\newcommand{\F}{\mathcal{F}}
1.17 +\newcommand{\Prop}{\mathcal{P}}
1.18 +
1.19 \title{\uppercase{\textbf{\Large{A}\large{lgorithmic} \Large{V}\large{erification of} \Large{R}\large{eactive} \Large{S}\large{ystems}}\\
1.20 \tiny{Draft}
1.21 }}
1.22 \author{
1.23 -\uppercase{{\small{E}\scriptsize{UGEN} \small{S}\scriptsize{AWIN}}\thanks{\texttt{sawine@informatik.uni-freiburg.de}}\\
1.24 -{\em \small{U}\scriptsize{NIVERSITY OF} \small{F}\scriptsize{REIBURG}}\\
1.25 +\uppercase{{\small{E}\scriptsize{UGEN} \small{S}\scriptsize{AWIN}}\thanks{\lowercase{\scriptsize{\texttt{sawine@informatik.uni-freiburg.de}}}}\\
1.26 +{\em \small{U}\scriptsize{NIVERSITY OF} \small{F}\scriptsize{REIBURG}}\thanks{\tiny{Computer Science Department, Research Group for Foundations of Artificial Intelligence}}\\
1.27 %{\em \small{C}\scriptsize{omputer} \small{S}\scriptsize{cience} \small{D}\scriptsize{epartment}}\\
1.28 {\em \small{G}\scriptsize{ERMANY}}}\\
1.29 %\texttt{\footnotesize{sawine@informatik.uni-freiburg.de}}
1.30 @@ -36,6 +42,7 @@
1.31 \newtheorem*{def:automata runs}{Runs}
1.32 \newtheorem*{def:automata acceptance}{Acceptance}
1.33 \newtheorem*{def:vocabulary}{Vocabulary}
1.34 +\newtheorem*{def:frames}{Frames}
1.35 \newtheorem*{def:models}{Models}
1.36 \newtheorem*{def:satisfiability}{Satisfiability}
1.37
1.38 @@ -143,7 +150,7 @@
1.39
1.40 A deterministic B\"uchi automaton is a specialisation where the \emph{transition relation} $\Delta$ is a \emph{transition function} $\delta: S \times \Sigma \to S$ and the set $S_0$ of \emph{initial states} contains only a single state $s_0$.
1.41
1.42 -Within this text \emph{automata/automaton} will refer to non-deterministic B\"uchi automata/automaton, unless otherwise noted.
1.43 +Within this text \emph{automaton} will refer to the non-deterministic B\"uchi automaton, unless otherwise noted.
1.44 \end{def:buechi automata}
1.45
1.46 \begin{def:automata runs}
1.47 @@ -157,9 +164,9 @@
1.48 \end{def:automata acceptance}
1.49
1.50 \section{Linear temporal logic}
1.51 -\subsection{Sytnax}
1.52 -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.53 -\[\varphi ::= p \in \mathcal{P} \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, X \varphi \,|\, \varphi U \varphi\]
1.54 +\subsection{Syntax}
1.55 +Let $\Prop$ be the countable set of \emph{atomic propositions}. The \emph{alphabet} of the language $L_{LTL}(\Prop)$ is $\Prop \cup \{\neg, \lor, X, U\}$. We define the $L_{LTL}(\Prop)$-\emph{formulae} $\varphi$ using following productions:
1.56 +\[\varphi ::= p \in \Prop \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, X \varphi \,|\, \varphi U \varphi\]
1.57
1.58 \subsection{Interpretation}
1.59 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.60 @@ -167,14 +174,19 @@
1.61 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.62
1.63 \subsection{Semantics}
1.64 +\begin{def:frames}
1.65 +A LTL-\emph{frame} is a tuple $\F = (S, R)$, where $S = \{s_i \mid i \in \N\}$ is the set of states and $R = \{(s_i, s_{i+1}) \mid i \in \N\}$ the set of accessibility relations. Hence $S$ is an isomorphism of $\N$ and $R$ an isomorphism of the strict linear order $(\N, <)$, which corresponds to the linear progression of time.
1.66 +\end{def:frames}
1.67 +
1.68 \begin{def:models}
1.69 -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.70 +A LTL-\emph{model} is a tuple $\M = (\F, V)$, where $\F$ is a \emph{frame} and $V: S \to 2^\Prop$ a \emph{valuation function}. Intuitively we say $p \in \Prop$ is \emph{true} at time instant $i$ iff $p \in V(i)$.
1.71 +%A \emph{model} is a function $\M: \N \to 2^\Prop$ over \emph{frame} $\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 \Prop$ is \emph{true} at time instant $i$ iff $p \in \M(i)$.
1.72 \end{def:models}
1.73
1.74 \begin{def:satisfiability}
1.75 -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.76 +A model $\M = (\F, V)$ \emph{satisfies} a 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.77 \begin{itemize}
1.78 -\item $\M,i \models p$ for $p \in \mathcal{P}$ iff $p \in \M(i)$
1.79 +\item $\M,i \models p$ for $p \in \Prop$ iff $p \in V(i)$
1.80 \item $\M,i \models \neg \varphi$ iff not $\M,i \models \varphi$
1.81 \item $\M,i \models \varphi \lor \psi$ iff $\M,i \models \varphi$ or $\M,i \models \psi$
1.82 \item $\M,i \models X \varphi$ iff $\M,i+1 \models \varphi$
1.83 @@ -183,10 +195,10 @@
1.84 \end{def:satisfiability}
1.85
1.86 \begin{def:vocabulary}
1.87 -Let $\varphi$ be a LTL-formula over atomic propositions $\mathcal{P}$, we define the \emph{vocabulary} $Voc(\varphi)$ of $\varphi$ inductively:
1.88 +Let $\varphi$ be a LTL-formula over atomic propositions $\Prop$, we define the \emph{vocabulary} $Voc(\varphi)$ of $\varphi$ inductively:
1.89 \begin{multicols}{2}
1.90 \begin{itemize}
1.91 -\item $Voc(p) = \{p\}$ for $p \in \mathcal{P}$
1.92 +\item $Voc(p) = \{p\}$ for $p \in \Prop$
1.93 \item $Voc(\neg \varphi) = Voc(\varphi)$
1.94 \item $Voc(\varphi \lor \psi) = Voc(\varphi) \cup Voc(\psi)$
1.95 \item $Voc(X \varphi) = Voc(\varphi)$
1.96 @@ -203,13 +215,13 @@
1.97 \[\forall{i \in \N}: \M,i \models \varphi \iff \M_{Voc(\varphi)},i \models \varphi\]
1.98 \end{prop:vocabulary sat}
1.99 %
1.100 -\subsection*{Derived connectives}
1.101 +\subsection{Derived connectives}
1.102 For a more convenient description of system specifications we present some derived symbols to be used in LTL-formulae. At first we introduce the notion of \emph{truth} and \emph{falsity} using constants $\top$ and $\bot$. Then we expand our set of connectives with the Boolean \emph{and}, \emph{implication} and \emph{equivalence}. And at last we derive the commonly used modal operators \emph{eventually} and \emph{henceforth}.
1.103
1.104 -Let $\varphi$ and $\psi$ be $L_{LTL}(\mathcal{P})$-formulae:
1.105 +Let $\varphi$ and $\psi$ be $L_{LTL}(\Prop)$-formulae:
1.106 \begin{multicols}{2}
1.107 \begin{itemize}
1.108 -\item $\top \equiv p \lor \neg p$ for $p \in \mathcal{P}$
1.109 +\item $\top \equiv p \lor \neg p$ for $p \in \Prop$
1.110 \item $\bot \equiv \neg \top$
1.111 \item $\varphi \land \psi \equiv \neg (\neg \varphi \lor \neg \psi)$
1.112 \item $\varphi \rightarrow \psi \equiv \neg \varphi \lor \psi$
1.113 @@ -225,8 +237,15 @@
1.114 \item $\M,i \models \Box \varphi$ iff $\forall{k \geq i}: \M,k \models \varphi$
1.115 \end{itemize}
1.116 \end{multicols}
1.117 +
1.118 +With the additional derived connectives we get the following $L_{LTL}(\Prop)$-formulae productions:
1.119 +\[\varphi ::= p \in \Prop \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, \varphi \land \varphi \,|\, X \varphi \,|\, \varphi U \varphi \,|\, \varphi \rightarrow \varphi \,|\, \varphi \leftrightarrow \varphi \,|\, \Diamond \varphi \,|\, \Box \varphi\]
1.120 +
1.121 \section{Model checking}
1.122
1.123 +
1.124 +\section{On-the-fly methods}
1.125 +
1.126 \begin{thebibliography}{99}
1.127 \bibitem{ref:ltl&büchi}
1.128 \uppercase{M{\footnotesize adhavan} M{\footnotesize ukund}.}
1.129 @@ -239,6 +258,11 @@
1.130 {\em Handbook of Modal Logic (Studies in Logic and Practical Reasoning)}.
1.131 3rd Edition, Elsevier, Amsterdam, 2007.
1.132
1.133 +\bibitem{ref:alternating verification}
1.134 +\uppercase{M{\footnotesize oshe} Y. V{\footnotesize ardi}.}
1.135 +{\em Alternating Automata and Program Verification}.
1.136 +Computer Science Today, Volume 1000 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1995.
1.137 +
1.138 \bibitem{ref:infpaths}
1.139 \uppercase{P{\footnotesize ierre} W{\footnotesize olper},
1.140 M{\footnotesize oshe} Y. V{\footnotesize ardi and}