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@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@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@15: \theoremstyle{definition} %plain, definition, remark, proposition, proof, corrolary
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@14: \newtheorem*{def:vocabulary}{Vocabulary}
sawine@19: \newtheorem*{def:frames}{Frames}
sawine@18: \newtheorem*{def:models}{Models}
sawine@18: \newtheorem*{def:satisfiability}{Satisfiability}
sawine@14: 
sawine@15: \theoremstyle{proposition}
sawine@14: \newtheorem{prop:vocabulary sat}{Proposition}
sawine@15: 
sawine@0: \begin{document}
sawine@0: \maketitle
sawine@4: \thispagestyle{empty}
sawine@2: %\itshape
sawine@2: %\renewcommand\abstractname{Abstract} 
sawine@0: \begin{abstract}
sawine@0: Over the past two decades, temporal logic has become a very basic tool for spec-
sawine@0: ifying properties of reactive systems. For finite-state systems, it is possible to use
sawine@0: techniques based on B\"uchi automata to verify if a system meets its specifications.
sawine@0: This is done by synthesizing an automaton which generates all possible models of
sawine@0: the given specification and then verifying if the given system refines this most gen-
sawine@0: eral automaton. In these notes, we present a self-contained introduction to the basic
sawine@0: techniques used for this automated verification. We also describe some recent space-
sawine@0: efficient techniques which work on-the-fly.
sawine@0: \end{abstract}
sawine@2: %\normalfont
sawine@4: \newpage
sawine@2: \section{Introduction}
sawine@2: Program verification is a fundamental area of study in computer science. The broad goal
sawine@5: is to verify whether a program is ``correct''--i.e., whether the implementation of a program
sawine@2: meets its specification. This is, in general, too ambitious a goal and several assumptions
sawine@2: have to be made in order to render the problem tractable. In these lectures, we will focus
sawine@2: on the verification of finite-state reactive programs. For specifying properties of programs,
sawine@2: we use linear time temporal logic.
sawine@2: 
sawine@2: What is a reactive program? The general pattern along which a conventional program
sawine@2: executes is the following: it accepts an input, performs some computation, and yields an
sawine@2: output. Thus, such a program can be viewed as an abstract function from an input domain
sawine@2: to an output domain whose behaviour consists of a transformation from initial states to
sawine@2: final states.
sawine@2: 
sawine@2: In contrast, a reactive program is not expected to terminate. As the name suggests, such
sawine@2: systems “react” to their environment on a continuous basis, responding appropriately to
sawine@2: each input. Examples of such systems include operating systems, schedulers, discrete-event
sawine@2: controllers etc. (Often, reactive systems are complex distributed programs, so concurrency
sawine@2: also has to be taken into account. We will not stress on this aspect in these lectures—we
sawine@2: take the view that a run of a distributed system can be represented as a sequence, by
sawine@2: arbitrarily interleaving concurrent actions.)
sawine@2: 
sawine@2: To specify the behaviour of a reactive system, we need a mechanism for talking about
sawine@2: the way the system evolves along potentially infinite computations. Temporal logic 
sawine@2: has become a well-established formalism for this purpose. Many varieties of temporal logic
sawine@2: have been defined in the past twenty years—we focus on propositional linear time temporal
sawine@2: logic (LTL).
sawine@2: 
sawine@2: There is an intimate connection between models of LTL formulas and languages of
sawine@2: infinite words—the models of an LTL formula constitute an ω-regular language over an
sawine@2: appropriate alphabet. As a result, the satisfiability problem for LTL reduces to checking
sawine@2: for emptiness of ω-regular languages. This connection was first explicitly pointed out in.
sawine@2: 
sawine@8: \section{$\omega$-regular languages}
sawine@7: \begin{def:finite words}
sawine@11: 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@17: $\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@15: 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@11: 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$.
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@17: 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@17: 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@15: 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$.
sawine@11: \end{def:automata acceptance}
sawine@11: 
sawine@8: \section{Linear temporal logic}
sawine@19: \subsection{Syntax}
sawine@19: 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@19: \[\varphi ::= p \in \Prop \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, X \varphi \,|\, \varphi U \varphi\]
sawine@13: 
sawine@18: \subsection{Interpretation}
sawine@13: 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@19: 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. 
sawine@19: \end{def:frames}
sawine@19: 
sawine@18: \begin{def:models}
sawine@19: 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)$. 
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@19: \item $\M,i \models p$ for $p \in \Prop$ iff $p \in V(i)$
sawine@17: \item $\M,i \models \neg \varphi$ iff not $\M,i \models \varphi$
sawine@17: \item $\M,i \models \varphi \lor \psi$ iff $\M,i \models \varphi$ or $\M,i \models \psi$
sawine@17: \item $\M,i \models X \varphi$ iff $\M,i+1 \models \varphi$
sawine@17: \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@18: \end{def:satisfiability}
sawine@18: 
sawine@14: \begin{def:vocabulary}
sawine@19: Let $\varphi$ be a 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@14: \item $Voc(X \varphi) = Voc(\varphi)$
sawine@14: \item $Voc(\varphi U \psi) = Voc(\varphi) \cup Voc(\psi)$
sawine@14: \end{itemize}
sawine@15: \end{multicols}
sawine@17: %
sawine@17: \noindent Let $\M$ be a model and $\varphi$ a LTL-formula, we define model $\M_{Voc(\varphi)}$:
sawine@17: \[\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@17: Let $\M$ be a model and $\varphi$ a LTL-formula, then following holds:
sawine@17: \[\forall{i \in \N}: \M,i \models \varphi \iff \M_{Voc(\varphi)},i \models \varphi\] 
sawine@17: \end{prop:vocabulary sat}
sawine@17: %
sawine@19: \subsection{Derived connectives}
sawine@17: 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@15: \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@16: 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@17: \item $\M,i \models \Diamond \varphi$ iff $\exists{k \geq i}: \M,k \models \varphi$
sawine@17: \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@19: With the additional derived connectives we get the following $L_{LTL}(\Prop)$-formulae productions:
sawine@19: \[\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@8: \section{Model checking}
sawine@15: 
sawine@19: 
sawine@19: \section{On-the-fly methods}
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@2: \bibitem{ref:handbook} 
sawine@6: \uppercase{P{\footnotesize atrick} B{\footnotesize lackburn}, 
sawine@6: F{\footnotesize rank} W{\footnotesize olter and} J{\footnotesize ohan van} B{\footnotesize enthem}.}
sawine@2: {\em Handbook of Modal Logic (Studies in Logic and Practical Reasoning)}.
sawine@3: 3rd Edition, Elsevier, Amsterdam, 2007.
sawine@7: 
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@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@0: \end{thebibliography}
sawine@0: \end{document}