sawine@7: \documentclass[a4paper, pagesize, DIV=calc, smallheadings]{article}  
sawine@2: \usepackage{graphicx}
sawine@2: %\usepackage[latin1]{inputenc}
sawine@14: \usepackage{amsmath, amsthm, amssymb, amsfonts, verbatim}
sawine@2: \usepackage{typearea}
sawine@2: \usepackage{algorithm}
sawine@2: \usepackage{algorithmic}
sawine@15: \usepackage{multicol}
sawine@11: %\usepackage{fullpage}
sawine@19: %\usepackage{a4wide}
sawine@19: \usepackage[left=3.9cm, right=3.9cm]{geometry}
sawine@5: %\usepackage[T1]{fontenc}
sawine@5: %\usepackage{arev}
sawine@7: %\pagestyle{headings}
sawine@19: 
sawine@2: \renewcommand{\familydefault}{\sfdefault}
sawine@22: \renewenvironment{proof}{{\bfseries Proof.}}{}
sawine@17: \newcommand{\M}{\mathcal{M}}
sawine@17: \newcommand{\N}{\mathbb{N}_0}
sawine@19: \newcommand{\F}{\mathcal{F}}
sawine@19: \newcommand{\Prop}{\mathcal{P}}
sawine@22: \newcommand{\A}{\mathcal{A}}
sawine@31: \newcommand{\X}{\mathcal{X}}
sawine@31: \newcommand{\U}{\mathcal{U}}
sawine@31: \newcommand{\V}{\mathcal{V}}
sawine@31: \newcommand{\dnf}{\mathsf{dnf}}
sawine@19: 
sawine@7: \title{\uppercase{\textbf{\Large{A}\large{lgorithmic} \Large{V}\large{erification of} \Large{R}\large{eactive} \Large{S}\large{ystems}}\\
sawine@7: \tiny{Draft}
sawine@7: }}
sawine@7: \author{
sawine@19: \uppercase{{\small{E}\scriptsize{UGEN} \small{S}\scriptsize{AWIN}}\thanks{\lowercase{\scriptsize{\texttt{sawine@informatik.uni-freiburg.de}}}}\\
sawine@19: {\em \small{U}\scriptsize{NIVERSITY OF} \small{F}\scriptsize{REIBURG}}\thanks{\tiny{Computer Science Department, Research Group for Foundations of Artificial Intelligence}}\\
sawine@7: %{\em \small{C}\scriptsize{omputer} \small{S}\scriptsize{cience} \small{D}\scriptsize{epartment}}\\
sawine@7: {\em \small{G}\scriptsize{ERMANY}}}\\
sawine@7: %\texttt{\footnotesize{sawine@informatik.uni-freiburg.de}}
sawine@7: }
sawine@5: \date{\textsc{\hfill}}
sawine@7: 
sawine@24: \theoremstyle{definition} %plain, definition, remark, proof, corollary
sawine@7: \newtheorem*{def:finite words}{Finite words}
sawine@7: \newtheorem*{def:infinite words}{Infinite words}
sawine@8: \newtheorem*{def:regular languages}{Regular languages}
sawine@8: \newtheorem*{def:regular languages closure}{Regular closure}
sawine@7: \newtheorem*{def:omega regular languages}{$\omega$-regular languages}
sawine@8: \newtheorem*{def:omega regular languages closure}{$\omega$-regular closure}
sawine@11: \newtheorem*{def:buechi automata}{Automata}
sawine@11: \newtheorem*{def:automata runs}{Runs}
sawine@11: \newtheorem*{def:automata acceptance}{Acceptance}
sawine@21: \newtheorem*{def:general automata}{Generalised automata}
sawine@21: \newtheorem*{def:general acceptance}{Acceptance}
sawine@14: \newtheorem*{def:vocabulary}{Vocabulary}
sawine@19: \newtheorem*{def:frames}{Frames}
sawine@18: \newtheorem*{def:models}{Models}
sawine@18: \newtheorem*{def:satisfiability}{Satisfiability}
sawine@30: \newtheorem*{def:fs closure}{Closure}
sawine@22: \newtheorem*{def:atoms}{Atoms}
sawine@28: \newtheorem*{def:rep function}{Representation function}
sawine@31: \newtheorem*{def:next}{Next function}
sawine@31: \newtheorem*{def:dnf}{Dijunctive normal form}
sawine@31: \newtheorem*{def:positive formulae}{Positive formulae}
sawine@14: 
sawine@22: \theoremstyle{plain}
sawine@21: \newtheorem{prop:vocabulary sat}{Proposition}[section]
sawine@21: \newtheorem{prop:general equiv}{Proposition}[section]
sawine@29: \newtheorem{prop:computation set=language}{Proposition}[section]
sawine@15: 
sawine@22: \theoremstyle{plain}
sawine@22: \newtheorem{thm:model language}{Theorem}[section]
sawine@24: \newtheorem{cor:mod=model language}{Corollary}[thm:model language]
sawine@29: \newtheorem{cor:mod=program language}[cor:mod=model language]{Corollary}
sawine@30: \newtheorem{thm:model checking}{Theorem}[section]
sawine@31: \newtheorem{lem:dnf}{Lemma}[section]
sawine@22: 
sawine@0: \begin{document}
sawine@0: \maketitle
sawine@4: \thispagestyle{empty}
sawine@2: %\itshape
sawine@2: %\renewcommand\abstractname{Abstract} 
sawine@0: \begin{abstract}
sawine@28: The algorithmic verification of reactive systems is based on automata-theoretic model checking. Linear temporal logic accommodates the capability for the characterisation of program specifications. For formulae composed in linear temporal logic, it is possible to construct B\"uchi automata constituting the model space of the specification. The verification of reactive systems is composed of such constructions and intersections of the program and specification automata. This paper provides an introduction to the construction techniques of automata and space-efficient on-the-fly verification methods for reactive systems. 
sawine@0: \end{abstract}
sawine@2: %\normalfont
sawine@4: \newpage
sawine@2: \section{Introduction}
sawine@2: 
sawine@2: 
sawine@8: \section{$\omega$-regular languages}
sawine@7: \begin{def:finite words}
sawine@24: Let $\Sigma$ be a non-empty set of symbols, called the alphabet. $\Sigma^*$ is the set of all \emph{finite} words over $\Sigma$. A \emph{finite} word $w \in \Sigma^*$ is a \emph{finite} sequence $(v_0,...,v_{n-1})$ of symbols from alphabet $\Sigma$ with length $n = |w|$. $\varepsilon$ denotes the empty word with length $|\varepsilon| = 0$.
sawine@7: \end{def:finite words}
sawine@7: 
sawine@8: \begin{def:regular languages}
sawine@8: The class of regular languages is defined recursively over an alphabet $\Sigma$:
sawine@15: \begin{multicols}{2}
sawine@8: \begin{itemize}
sawine@8: \item $\emptyset$ is regular
sawine@8: \item $\{\varepsilon\}$ is regular
sawine@8: \item $\forall_{a \in \Sigma}:\{a\}$ is regular
sawine@8: \end{itemize}
sawine@15: \end{multicols}
sawine@8: \end{def:regular languages}
sawine@8: 
sawine@8: \begin{def:regular languages closure}
sawine@10: Let $L_{R_1}, L_{R_2} \in \Sigma^*$ be regular. The class of regular languages is closed under following operations:
sawine@15: \begin{multicols}{2}
sawine@8: \begin{itemize}
sawine@8: \item $L_{R_1}^*$
sawine@8: \item $L_{R_1} \circ L_{R_2}$
sawine@8: \item $L_{R_1} \cup L_{R_2}$
sawine@10: \item $L_{R_1} \cap L_{R_2}$
sawine@10: \item $\overline{L}_{R_1}$ and therefore $L_{R_1} - L_{R_2}$
sawine@8: \end{itemize}
sawine@15: \end{multicols}
sawine@8: \end{def:regular languages closure}
sawine@8: 
sawine@9: \begin{def:infinite words}
sawine@24: $\Sigma^\omega$ is the set of all \emph{infinite} words over $\Sigma$. An \emph{infinite} word $w \in \Sigma^\omega$ is an \emph{infinite} sequence $(v_0,...,v_\infty)$ with length $\infty$. To address the elements of the infinite sequence $w$, we view the word as a function $w : \N \to \Sigma$ with $w(i) = v_i$; thus $w(i)$ denotes the symbol at sequence position $i$ of word $w$; another notation used for $w(i)$ is $w_i$.
sawine@9: \end{def:infinite words}
sawine@9: 
sawine@7: \begin{def:omega regular languages}
sawine@8: Set $L$ is an $\omega$-language over alphabet $\Sigma$ iff $L \subseteq \Sigma^\omega$. Let $L_R \subseteq \Sigma^*$ be a non-empty regular finite language and $\varepsilon \notin L_R$. A set $L$ is $\omega$-regular iff $L$ is an $\omega$-language and $L = L_R^\omega$.
sawine@7: \end{def:omega regular languages}
sawine@7: 
sawine@8: \begin{def:omega regular languages closure}
sawine@8: Let $L_{\omega_1}, L_{\omega_2} \subseteq \Sigma^\omega$ be $\omega$-regular languages. The class of $\omega$-regular languages is closed under following operations:
sawine@8: \begin{itemize}
sawine@8: \item $L_R \circ L_{\omega_1}$, but \emph{not} $L_{\omega_1} \circ L_R$
sawine@8: \item $L_{\omega_1} \cup L_{\omega_2}$, but only \emph{finitely} many times
sawine@8: \end{itemize}
sawine@8: \end{def:omega regular languages closure}
sawine@7: 
sawine@8: \section{B\"uchi automata}
sawine@11: \begin{def:buechi automata}
sawine@22: A non-deterministic B\"uchi automaton is a tuple $\A = (\Sigma, S, S_0, \Delta, F)$, where $\Sigma$ is a finite non-empty \emph{alphabet}, $S$ is a finite non-empty set of \emph{states}, $S_0 \subseteq S$ is the set of \emph{initial states}, $F \subseteq S$ is the set of \emph{accepting states} and $\Delta: S \times \Sigma \times S$ is a \emph{transition relation}. When suitable we will use the arrow notation for the transitions, where $s \xrightarrow{a} s'$ iff $(s, a, s') \in \Delta$.
sawine@11: 
sawine@22: A \emph{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$.
sawine@11: 
sawine@19: Within this text \emph{automaton} will refer to the non-deterministic B\"uchi automaton, unless otherwise noted. 
sawine@11: \end{def:buechi automata}
sawine@11: 
sawine@11: \begin{def:automata runs}
sawine@24: Let $\A = (\Sigma, S, S_0, \Delta, F)$ be an automaton, a run $\rho$ of $\A$ on an infinite word $w = (a_0,a_1,...)$ over alphabet $\Sigma$ is a sequence $\rho = (s_0,s_1,...)$, where $s_0 \in S_0$ and $(s_i, a_i, s_{i+1}) \in \Delta$, for all $i \geq 0$. Again we may view the run sequence as a function $\rho : \N \to S$, where $\rho(i) = s_i$ denotes the state at the $i^{th}$ sequence position.
sawine@11: \end{def:automata runs}
sawine@11: 
sawine@11: \begin{def:automata acceptance}
sawine@22: 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 \N}: \rho(n) = s\}$, where $\exists^\omega$ denotes the existential quantifier for infinitely many occurances, i.e., $s$ occurs infinitely often in $\rho$.
sawine@11: 
sawine@22: 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}. 
sawine@21: 
sawine@22: The language $L_\omega(\A)$ recognised by automaton $\A$ is the set of all infinite words accepted by $\A$. A language $L$ is \emph{B\"uchi-recognisable} iff there is an automaton $\A$ with $L = L_\omega(\A)$.
sawine@11: \end{def:automata acceptance}
sawine@11: 
sawine@21: \subsection{Generalised B\"uchi automata}
sawine@21: \begin{def:general automata}
sawine@22: A \emph{generalised B\"uchi automaton} is a tuple $\A = (\Sigma, S, S_0, \Delta, \{F_i\}_{i < k})$ for $i, k \in \N$, where the \emph{acceppting states} $F_i$ are composed within a finite set with $F_i \subseteq S$.
sawine@21: \end{def:general automata}
sawine@21: 
sawine@21: \begin{def:general acceptance}
sawine@22: The acceptance condition is adjusted accordingly. A run $\rho$ of $\A$ is \emph{accepting} iff $\forall{i < k}: inf(\rho) \cap F_i \neq \emptyset$. 
sawine@21: \end{def:general acceptance}
sawine@21: 
sawine@21: \begin{prop:general equiv}
sawine@22: Let $\A = (\Sigma, S, S_0, \Delta, \{F_i\}_{i < k})$ be a \emph{generalised automaton} and let $\A_i = (\Sigma, S, S_0, \Delta, F_i)$ be \emph{non-deterministic automata}, then following equivalance condition holds:
sawine@29: \[L_\omega(\A) = \bigcap_{i < k} L_\omega(\A_i)\]
sawine@21: \end{prop:general equiv}
sawine@21: \noindent Intuitively follows the equivalance of the language recognition abilities of general and non-deterministic B\"uchi automata.
sawine@21: 
sawine@8: \section{Linear temporal logic}
sawine@19: \subsection{Syntax}
sawine@31: 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:
sawine@31: \[\varphi ::= p \in \Prop \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, \X \varphi \,|\, \varphi \U \varphi\]
sawine@13: 
sawine@18: \subsection{Interpretation}
sawine@31: 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}.
sawine@13: 
sawine@13: 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.
sawine@13: 
sawine@18: \subsection{Semantics}
sawine@19: \begin{def:frames}
sawine@22: An 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 discrete time. 
sawine@19: \end{def:frames}
sawine@19: 
sawine@18: \begin{def:models}
sawine@22: An 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)$. 
sawine@19: %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)$.
sawine@18: \end{def:models}
sawine@13: 
sawine@18: \begin{def:satisfiability}
sawine@19: 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$:
sawine@13: \begin{itemize}
sawine@22: \item $\M,i \models p$ for $p \in \Prop \iff p \in V(i)$
sawine@22: \item $\M,i \models \neg \varphi \iff$ not $\M,i \models \varphi$
sawine@22: \item $\M,i \models \varphi \lor \psi \iff \M,i \models \varphi$ or $\M,i \models \psi$
sawine@31: \item $\M,i \models \X \varphi \iff \M,i+1 \models \varphi$
sawine@31: \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$
sawine@13: \end{itemize}
sawine@22: 
sawine@18: \end{def:satisfiability}
sawine@18: 
sawine@14: \begin{def:vocabulary}
sawine@22: Let $\varphi$ be an LTL-formula over atomic propositions $\Prop$, we define the \emph{vocabulary} $Voc(\varphi)$ of $\varphi$ inductively:
sawine@15: \begin{multicols}{2}
sawine@14: \begin{itemize}
sawine@19: \item $Voc(p) = \{p\}$ for $p \in \Prop$
sawine@14: \item $Voc(\neg \varphi) = Voc(\varphi)$
sawine@14: \item $Voc(\varphi \lor \psi) = Voc(\varphi) \cup Voc(\psi)$
sawine@31: \item $Voc(\X \varphi) = Voc(\varphi)$
sawine@31: \item $Voc(\varphi \U \psi) = Voc(\varphi) \cup Voc(\psi)$
sawine@14: \end{itemize}
sawine@15: \end{multicols}
sawine@17: %
sawine@22: \noindent Let $\M = (\F, V)$ be a model and $\varphi$ an LTL-formula, we define model $\M_{Voc(\varphi)} = (\F, V_{Voc(\varphi)})$ with:
sawine@21: \[\forall{i \in \N}: V_{Voc(\varphi)}(i) = V(i) \cap Voc(\varphi)\]
sawine@21: Henceforth, we will abbreviate $\M_{Voc(\varphi)}$ and $V_{Voc(\varphi)}$ with $\M_\varphi$ and $V_\varphi$ accordingly. 
sawine@22: %\noindent Let $\M$ be a model and $\varphi$ an LTL-formula, we define model $\M_{Voc(\varphi)}$:
sawine@21: %\[\forall{i \in \N}: \M_{Voc(\varphi)} = \M(i) \cap Voc(\varphi)\]
sawine@17: \end{def:vocabulary}
sawine@17: %
sawine@17: \begin{prop:vocabulary sat}
sawine@22: Let $\M$ be a model and $\varphi$ an LTL-formula, then following holds:
sawine@21: \[\forall{i \in \N}: \M,i \models \varphi \iff \M_\varphi,i \models \varphi\] 
sawine@17: \end{prop:vocabulary sat}
sawine@17: %
sawine@19: \subsection{Derived connectives}
sawine@31: 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}. 
sawine@15: 
sawine@19: Let $\varphi$ and $\psi$ be $L_{LTL}(\Prop)$-formulae:
sawine@15: \begin{multicols}{2}
sawine@15: \begin{itemize}
sawine@19: \item $\top \equiv p \lor \neg p$ for $p \in \Prop$
sawine@15: \item $\bot \equiv \neg \top$
sawine@15: \item $\varphi \land \psi \equiv \neg (\neg \varphi \lor \neg \psi)$
sawine@15: \item $\varphi \rightarrow \psi \equiv \neg \varphi \lor \psi$
sawine@15: \item $\varphi \leftrightarrow \psi \equiv (\varphi \rightarrow \psi) \land (\psi \rightarrow \varphi)$
sawine@31: \item $\Diamond \varphi \equiv \top \U \varphi$
sawine@15: \item $\Box \varphi \equiv \neg \Diamond \neg \varphi$
sawine@15: \end{itemize}
sawine@15: \end{multicols}
sawine@28: \noindent From the derivations for operators $\Diamond$, \emph{read diamond}, and $\Box$, \emph{read box}, it follows:
sawine@17: \begin{multicols}{2}
sawine@16: \begin{itemize}
sawine@31: \item $\M,i \models \Diamond \varphi \iff \exists{k \geq i}: \M,k \models \varphi$
sawine@31: \item $\M,i \models \Box \varphi \iff \forall{k \geq i}: \M,k \models \varphi$
sawine@16: \end{itemize}
sawine@17: \end{multicols}
sawine@19: 
sawine@28: \noindent With the additional derived connectives we get the following $L_{LTL}(\Prop)$-formulae productions:
sawine@31: \[\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\]
sawine@19: 
sawine@21: \section{Automata construction}
sawine@28: Before applying the automata-theoretic verification methods, we need to construct the automaton for a given specification formula $\varphi$ and for the program $P$ in test.
sawine@24: 
sawine@28: \subsection{Specification automata}
sawine@28: For the construction of an automaton $\A_\varphi$ for an LTL-formula $\varphi$, we treat the model $\M = (\F, V)$ for an LTL-formula $\varphi$ as an infinite word over the finite alphabet $2^{Voc(\varphi)}$. 
sawine@28: 
sawine@28: \begin{def:rep function}
sawine@24: We define the \emph{representation function} $rep: \M \to 2^\Prop$, which returns an infinite word representing the model $\M_\varphi = (\F, V_\varphi)$ over the ordered image $V_\varphi^\rightarrow(\N)$ of its validation function, i.e., $rep(\M_\varphi) = (V_\varphi(0), V_\varphi(1), ...)$. Additionaly, we provide the \emph{inverted representation function} $rep^{-1}: 2^\Prop \to \M$, which compiles an infinite word to the corresponding model, i.e., $rep^{-1}(V_\varphi^\rightarrow(\N)) = \M_\varphi$.
sawine@22: \[Mod(\varphi) = \{rep(\M_\varphi) \mid \M_\varphi = (\F, V_\varphi) \land \M_\varphi,0 \models \varphi\}\]
sawine@21: $Mod(\varphi)$ is the set of all infinite words, which represent models for $\varphi$.
sawine@28: \end{def:rep function}
sawine@21: 
sawine@22: \begin{def:fs closure}
sawine@30: Let $\varphi$ be an LTL-formula, then the \emph{Fischer-Ladner closure} $CL(\varphi)$ of $\varphi$ is the smallest set of formulae such that following holds:
sawine@22: %\begin{multicols}{2}
sawine@22: \begin{itemize}
sawine@30: \item $\varphi \in CL(\varphi)$
sawine@30: \item $\neg \psi \in CL(\varphi) \implies \psi \in CL(\varphi)$
sawine@30: \item $\psi \in CL(\varphi) \implies \neg \psi \in CL(\varphi)$
sawine@30: \item $\psi \lor \chi \in CL(\varphi) \implies \psi, \chi \in CL(\varphi)$
sawine@31: \item $\X \psi \in CL(\varphi) \implies \psi \in CL(\varphi)$
sawine@31: \item $\psi \U \chi \in CL(\varphi) \implies \psi, \chi, \X(\psi \U \chi) \in CL(\varphi)$
sawine@22: \end{itemize}
sawine@22: %\end{multicols}
sawine@22: \end{def:fs closure}
sawine@22: 
sawine@30: \noindent Let $CL(\varphi)$ be the closure of formula $\varphi$, we define a subset with the \emph{until}-formulae of the closure $\mathbb{U}_\varphi \subseteq CL(\varphi)$ where:
sawine@31: \[\mathbb{U}_\varphi = \{\psi \U \chi \in CL(\varphi)\} \text{ and } \mathbb{U}_{\varphi_i} \text{ denotes the $i^{th}$ element of } \mathbb{U_\varphi}\]
sawine@22: 
sawine@22: \begin{def:atoms}
sawine@30: Let $\varphi$ be a formula and $CL(\varphi)$ its closure. $A \subseteq CL(\varphi)$ is an \emph{atom} if following holds:
sawine@22: \begin{itemize}
sawine@30: \item $\forall{\psi \in CL(\varphi)}: \psi \in A \iff \neg \psi \notin A$
sawine@30: \item $\forall{\psi \lor \chi \in CL(\varphi)}: \psi \lor \chi \in A \iff \psi \in A$ or $\chi \in A$ 
sawine@31: \item $\forall{\psi \U \chi \in CL(\varphi)}: \psi \U \chi \in A \iff \chi \in A$ or $\psi, \X(\psi \U \chi) \in A$ 
sawine@22: \end{itemize}
sawine@30: We define the set of all atoms of formula $\varphi$ with $\mathbb{AT}_\varphi = \{A \subseteq CL({\varphi}) \mid A \text{ is an atom}\}$.
sawine@22: \end{def:atoms}
sawine@22: 
sawine@22: \noindent Now that we have the required ingredients, we begin with the construction of automaton $\A_\varphi$ for formula $\varphi$. Let $\A_\varphi = (\Sigma, S, S_0, \Delta, \{F_i\}_{i < k})$ with:
sawine@22: \begin{itemize}
sawine@22: \item $\Sigma = 2^{Voc(\varphi)}$
sawine@22: \item $S = \mathbb{AT_\varphi}$
sawine@23: \item $S_0 = \{A \in \mathbb{AT_\varphi} \mid \varphi \in A\}$
sawine@31: %\item $(A, P, B) \in \Delta$ for $A, B \in \mathbb{AT_\varphi}$ and $P = A \cap Voc(\varphi) \iff (\X \psi \in A \iff \psi \in B)$
sawine@31: \item $\Delta = \{(A, P, B) \mid A, B \in \mathbb{AT_\varphi}, P = A \cap Voc(\varphi), \X \psi \in A \iff \psi \in B\}$
sawine@31: %\item $\forall{i \in \N, i < k = |\mathbb{U}_{CL(\varphi)}|}: F_i = \{A \in \mathbb{AT}_\varphi \mid \psi \U \chi \notin A$ or $\chi \in A\}$
sawine@31: \item $F_i = \{A \in \mathbb{AT}_\varphi \mid \psi \U \chi = \mathbb{U}_{\varphi_i}, \psi \U \chi \notin A$ or $\chi \in A\}$ and therefore $k = |\mathbb{U}_{\varphi}|$
sawine@22: %Let $A, B \in \mathbb{AT}$ and $P \subseteq Voc(\varphi)$. Then $(A, P, B) \in \Delta$ iff the following holds:
sawine@31: %$P = A \cap Voc(\varphi)$ and For all $\X \psi \in CL(\varphi): \X \psi \in A$ iff $\psi \in B$.
sawine@22: \end{itemize}
sawine@22: 
sawine@22: \begin{thm:model language}
sawine@24: \label{thm:model language}
sawine@22: Let $\M_\varphi = (\F, V_\varphi)$ be a model and $rep(\M_\varphi)$ its infinite representation word, then following holds:
sawine@29: \[rep(\M_\varphi) \in L_\omega(\A_\varphi) \iff \M_\varphi,0 \models \varphi\]
sawine@22: \end{thm:model language}
sawine@22: \noindent
sawine@22: \begin{proof}
sawine@22: For the eloberate proof, consult \cite{ref:ltl&büchi}.
sawine@22: \end{proof}
sawine@24: \begin{cor:mod=model language}
sawine@24: \label{cor:mod=model language}
sawine@31: From Theorem \ref{thm:model language} follows $Mod(\varphi) = L_\omega(\A_\varphi)$.
sawine@24: \end{cor:mod=model language}
sawine@21: 
sawine@28: \subsection{Program automata}
sawine@28: In the next step, we model a given program $P$ as automaton $\A_P$. A program is a structure $P = (S_P, s_0, R, V)$, where $S$ is the set of possible states of the program, $s_0$ the initial state, $R : S \times \Prop \times S$ the transition relation and $V : S \to 2^\Prop$ a valuation function. A \emph{computation} of $P$ is a run $\rho = (V(s_0), V(s_1), ...)$. 
sawine@28: 
sawine@28: We construct automaton $\A_P = (\Sigma, S, S_0, \Delta, F)$, with:
sawine@28: \begin{itemize}
sawine@28: \begin{multicols}{2}
sawine@28: \item $\Sigma = 2^\Prop$
sawine@28: \item $S = S_P$
sawine@29: \item $S_0 = \{s_0\}$
sawine@28: \item $F = S$
sawine@28: \end{multicols}
sawine@28: \item $\Delta = \{(s, V(s), s') \mid \exists{a \in \Prop}: (s, a, s') \in R\}$
sawine@28: \end{itemize}
sawine@29: In practical verification of programs, the specification covers only the properties of a system, which are vital to the program's correctness, where our program description contains all details of all possible execution paths. Let $\varphi$ be the specification formula, we can reduce the state exploration to the vocabulary of $\varphi$ by the reduction of the transition relation to $\Delta = \{(s, A, s') \mid \exists{a \in \Prop}: (s, a, s') \in R \land A = V(s) \cap Voc(\varphi)\}$.
sawine@28: 
sawine@29: \begin{prop:computation set=language}
sawine@29: \label{prop:computation set=language}
sawine@29: Let $\A_P = (\Sigma, S, S_0, \Delta, F)$, for $F = S$ it follows that each run of $\A_P$ is accepting, therefore is $L_\omega(\A_P)$ the set of all computations of $P$.
sawine@29: \[L_\omega(\A_P) = \{\rho \mid \rho \text{ is a run of } \A_P\}\]
sawine@29: \end{prop:computation set=language}
sawine@29: 
sawine@29:  We can view each run of $\A_P$, i.e., each computation of $P$, as a representation of model $\M_\rho = (\F, V)$, where $\F$ is a frame and $V$ the program's valuation function. In analogy to the specification, we define:
sawine@29: \[Mod(P) = \{\rho \mid \rho \text{ is a computation of } P\}\]
sawine@29: \begin{cor:mod=program language}
sawine@29: \label{cor:mod=program language}
sawine@31: From Theorem \ref{thm:model language} and Proposition \ref{prop:computation set=language} follows $Mod(P) = L_\omega(\A_P)$.
sawine@29: \end{cor:mod=program language}
sawine@28: 
sawine@8: \section{Model checking}
sawine@29: For effective automata-theoretic verification of reactive programs, we have modelled the program as a non-deterministic B\"uchi automaton $\A_P$ and the specification formula $\varphi$ as automaton $\A_\varphi$. 
sawine@29: 
sawine@31: Given a program $P$ and specification $\varphi$, the verification problem is the following: \emph{does every run of $P$ satisfy $\varphi$?} To show this we use the previously introduced automata constructions and reduce the problem to $L_\omega(\A_P) \subseteq L_\omega(\A_\varphi)$, i.e., all runs accepted by $\A_P$ are also accepted by $\A_\varphi$. By this problem definition, we clearly have to explore the whole state space of $\A_\varphi$ for each run of $\A_P$. This prevents efficient on-demand constructions. Therefore we rephrase the problem with the contrapositive definition $L_\omega(\A_P) \cap \overline{L_\omega(\A_\varphi)} = \emptyset$, where $\overline{L_\omega(\A_\varphi)} = \Sigma^\omega - L_\omega(\A_\varphi) = L_\omega(\A_{\neg \varphi})$ \cite{ref:alternating verification}.
sawine@30: 
sawine@30: In conclusion, the essence of model checking lies within the test for emptyness of the intersection between the recognised language of the program automaton and the recognised language of the automaton for its negated specification:
sawine@29: \[L_\omega(\A_P) \cap L_\omega(\A_{\neg \varphi}) = \emptyset\]
sawine@30: 
sawine@30: \begin{thm:model checking}
sawine@30: \label{thm:model checking}
sawine@30: Let $P$ be a finite-state program and $\A_P$ its automaton, let $\varphi$ be an LTL-formula and $\A_\varphi$ its automaton. P satisfies $\varphi$ iff $L_\omega(\A_P) \cap L_\omega(\A_{\neg \varphi}) = \emptyset$.
sawine@30: \end{thm:model checking}
sawine@30: 
sawine@31: From Corollary \ref{cor:mod=model language} and \ref{cor:mod=program language} follows:
sawine@29: \[L_\omega(\A_P) \cap L_\omega(\A_{\neg \varphi}) = \emptyset \iff Mod(P) \cap Mod(\neg \varphi) = \emptyset\]
sawine@29: 
sawine@30: \subsection{Complexity}
sawine@31: Let the size $|P|$ of a program $P = (S, s_0, R, V)$ be proportional to the sum of its structural components, i.e., $|P| = |S| + |R|$. The size $|\varphi|$ is the length of the formula string. The asymptotical complexity of the presented automata-theoretic verification method is in time $O(|P| \cdot 2^{O(|\varphi|)})$ \cite{ref:concurrent checking}. 
sawine@30: 
sawine@31: The size of $\varphi$ is usually short \cite{ref:concurrent checking}, so the exponential growth by it is reasonable. Generally, the number of states is at least exponential in the size of its description by means of a programming language. This concludes, that despite that the upper bound is polynomial in the size of the program, in practice, we are facing exponential growth in complexity \cite{ref:handbook}.
sawine@19: 
sawine@19: \section{On-the-fly methods}
sawine@31: The automata-theoretic approach on verification in Theorem \ref{thm:model checking} requires a fully constructed automaton for the specification, when applying the graph-theoretic emptyness test. 
sawine@31: 
sawine@31: A more space-efficient strategy is the on-the-fly construction of the automaton during a depth-first search, short DFS. The DFS explores the product states of both automata incrementally, testing for cycles in each iteration. If the program does not satisfy a formula, an accepting cycle will occur and lead to termination of the search. In the case of a valid program, i.e., the program does meet the specification, no cycles will occur. In the latter case, such a strategy would inevitably explore the whole state space of the automata.
sawine@31: 
sawine@31: \begin{def:positive formulae}
sawine@31: Let $\Prop$ be a set of atomic propositions, let $\overline{\Prop} = \{\neg p \mid p \in \Prop\}$ and let us extend the LTL-syntax with the binary operator $\V$ with $\varphi \V \psi \equiv \neg(\neg \varphi \U \psi)$. We define the set of LTL-formulae in \emph{positive form}:
sawine@31: \[\Phi^+ = \Prop \cup \overline{\Prop} \cup \{\top, \bot\} \cup \{\varphi \lor \psi, \varphi \land \psi, \X\varphi, \varphi \U \psi, \varphi \V \psi \mid \varphi, \psi \in \Phi^+\} \]
sawine@31: \end{def:positive formulae}
sawine@31: 
sawine@31: \begin{def:next}
sawine@31: Let $\Phi$ be a set of LTL-formulae, we define:
sawine@31: \[next(\Phi) = \{ \X\varphi \mid \X\varphi \in \Phi\} \text{ and } snext(\Phi) = \{ \varphi \mid \X\varphi \in \Phi\}\]
sawine@31: \end{def:next}
sawine@31: 
sawine@31: \begin{def:dnf}
sawine@31: Let $\Phi^+$ be the set of LTL-formulae in positive form and let $Q = \Prop \cup \overline{\Prop} \cup next(\Phi^+)$, we define function $\dnf: \Phi^+ \to Q$ inductively:
sawine@31: \begin{align*}
sawine@31: &\dnf(\top) &=  &\, \{\emptyset\}\\
sawine@31: &\dnf(\bot) &= &\, \emptyset\\
sawine@31: &\dnf(x) &=  &\, \{\{x\}\}, \text{ for } x = p, \neg p, \X\varphi\\
sawine@31: &\dnf(\varphi \lor \psi) &=  &\, \dnf(\varphi) \cup \dnf(\psi)\\
sawine@31: &\dnf(\varphi \land \psi) &=  &\, \{C \cup D \mid C \in \dnf(\varphi), D \in \dnf(\psi), C \cup D \text{ is consistent}\}\\
sawine@31: &\dnf(\varphi \U \psi) &=  &\, \dnf(\varphi \land \X(\varphi \U \psi)) \cup \dnf(\psi)\\
sawine@31: &\dnf(\varphi \V \psi) &=  &\, \dnf(\varphi \land \psi) \cup \dnf(\psi \land \X(\varphi \V \psi))\\
sawine@31: \end{align*}
sawine@31: \end{def:dnf}
sawine@31: 
sawine@31: \begin{lem:dnf}
sawine@31: Let $\Phi^+$ be the set of formulae in positive form, following holds:
sawine@31: \[\forall{\varphi \in \Phi^+}: \varphi \iff \bigvee_{D \in \dnf(\varphi)} \bigwedge D\]
sawine@31: \end{lem:dnf}
sawine@19: 
sawine@0: \begin{thebibliography}{99}
sawine@5: \bibitem{ref:ltl&büchi} 
sawine@6: \uppercase{M{\footnotesize adhavan} M{\footnotesize ukund}.}
sawine@5: {\em Linear-Time Temporal Logic and B\"uchi Automata}.
sawine@2: Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, 1997.
sawine@0: 
sawine@19: \bibitem{ref:alternating verification} 
sawine@19: \uppercase{M{\footnotesize oshe} Y. V{\footnotesize ardi}.}
sawine@19: {\em Alternating Automata and Program Verification}.
sawine@19: Computer Science Today, Volume 1000 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1995.
sawine@19: 
sawine@30: \bibitem{ref:concurrent checking}
sawine@30: \uppercase{O{\footnotesize rna} L{\footnotesize ichtenstein and} A{\footnotesize mir} P{\footnotesize nueli}.}
sawine@30: {\em Checking that finite state concurrent programs satisfy their linear specification}.
sawine@30: Proceeding 12th ACM Symposium on Principles of Programming Languages, New York, 1985.
sawine@30: 
sawine@7: \bibitem{ref:infpaths}
sawine@7: \uppercase{P{\footnotesize ierre} W{\footnotesize olper}, 
sawine@7: M{\footnotesize oshe} Y. V{\footnotesize ardi and}
sawine@7: A. P{\footnotesize rasad} S{\footnotesize istla}.}
sawine@7: {\em Reasoning about Infinite Computation Paths}.
sawine@7: In Proceedings of the 24th IEEE FOCS, 1983.
sawine@7: 
sawine@30: \bibitem{ref:handbook} 
sawine@30: \uppercase{P{\footnotesize atrick} B{\footnotesize lackburn}, 
sawine@30: F{\footnotesize rank} W{\footnotesize olter and} J{\footnotesize ohan van} B{\footnotesize enthem}.}
sawine@30: {\em Handbook of Modal Logic (Studies in Logic and Practical Reasoning)}.
sawine@30: 3rd Edition, Elsevier, Amsterdam, 2007.
sawine@0: \end{thebibliography}
sawine@0: \end{document}