\documentclass[a4paper, pagesize, DIV=calc, smallheadings]{article}  

\usepackage{graphicx}

%\usepackage[latin1]{inputenc}

\usepackage{amsmath, amsthm, amssymb, amsfonts, verbatim}

\usepackage{typearea}

\usepackage{algorithm}

\usepackage{algorithmic}

\usepackage{multicol}

%\usepackage{fullpage}

%\usepackage{a4wide}

\usepackage[left=3.9cm, right=3.9cm]{geometry}

%\usepackage[T1]{fontenc}

%\usepackage{arev}

%\pagestyle{headings}

\renewcommand{\familydefault}{\sfdefault}

\newcommand{\M}{\mathcal{M}}

\newcommand{\N}{\mathbb{N}_0}

\newcommand{\F}{\mathcal{F}}

\newcommand{\Prop}{\mathcal{P}}

\title{\uppercase{\textbf{\Large{A}\large{lgorithmic} \Large{V}\large{erification of} \Large{R}\large{eactive} \Large{S}\large{ystems}}\\

\tiny{Draft}

}}

\author{

\uppercase{{\small{E}\scriptsize{UGEN} \small{S}\scriptsize{AWIN}}\thanks{\lowercase{\scriptsize{\texttt{sawine@informatik.uni-freiburg.de}}}}\\

{\em \small{U}\scriptsize{NIVERSITY OF} \small{F}\scriptsize{REIBURG}}\thanks{\tiny{Computer Science Department, Research Group for Foundations of Artificial Intelligence}}\\

%{\em \small{C}\scriptsize{omputer} \small{S}\scriptsize{cience} \small{D}\scriptsize{epartment}}\\

{\em \small{G}\scriptsize{ERMANY}}}\\

%\texttt{\footnotesize{sawine@informatik.uni-freiburg.de}}

}

\date{\textsc{\hfill}}

\theoremstyle{definition} %plain, definition, remark, proposition, proof, corrolary

\newtheorem*{def:finite words}{Finite words}

\newtheorem*{def:infinite words}{Infinite words}

\newtheorem*{def:regular languages}{Regular languages}

\newtheorem*{def:regular languages closure}{Regular closure}

\newtheorem*{def:omega regular languages}{$\omega$-regular languages}

\newtheorem*{def:omega regular languages closure}{$\omega$-regular closure}

\newtheorem*{def:buechi automata}{Automata}

\newtheorem*{def:automata runs}{Runs}

\newtheorem*{def:automata acceptance}{Acceptance}

\newtheorem*{def:general automata}{Generalised automata}

\newtheorem*{def:general acceptance}{Acceptance}

\newtheorem*{def:vocabulary}{Vocabulary}

\newtheorem*{def:frames}{Frames}

\newtheorem*{def:models}{Models}

\newtheorem*{def:satisfiability}{Satisfiability}

\theoremstyle{proposition}

\newtheorem{prop:vocabulary sat}{Proposition}[section]

\newtheorem{prop:general equiv}{Proposition}[section]

\begin{document}

\maketitle

\thispagestyle{empty}

%\itshape

%\renewcommand\abstractname{Abstract} 

\begin{abstract}

Over the past two decades, temporal logic has become a very basic tool for spec-

ifying properties of reactive systems. For finite-state systems, it is possible to use

techniques based on B\"uchi automata to verify if a system meets its specifications.

This is done by synthesizing an automaton which generates all possible models of

the given specification and then verifying if the given system refines this most gen-

eral automaton. In these notes, we present a self-contained introduction to the basic

techniques used for this automated verification. We also describe some recent space-

efficient techniques which work on-the-fly.

\end{abstract}

%\normalfont

\newpage

\section{Introduction}

Program verification is a fundamental area of study in computer science. The broad goal

is to verify whether a program is ``correct''--i.e., whether the implementation of a program

meets its specification. This is, in general, too ambitious a goal and several assumptions

have to be made in order to render the problem tractable. In these lectures, we will focus

on the verification of finite-state reactive programs. For specifying properties of programs,

we use linear time temporal logic.

What is a reactive program? The general pattern along which a conventional program

executes is the following: it accepts an input, performs some computation, and yields an

output. Thus, such a program can be viewed as an abstract function from an input domain

to an output domain whose behaviour consists of a transformation from initial states to

final states.

In contrast, a reactive program is not expected to terminate. As the name suggests, such

systems “react” to their environment on a continuous basis, responding appropriately to

each input. Examples of such systems include operating systems, schedulers, discrete-event

controllers etc. (Often, reactive systems are complex distributed programs, so concurrency

also has to be taken into account. We will not stress on this aspect in these lectures—we

take the view that a run of a distributed system can be represented as a sequence, by

arbitrarily interleaving concurrent actions.)

To specify the behaviour of a reactive system, we need a mechanism for talking about

the way the system evolves along potentially infinite computations. Temporal logic 

has become a well-established formalism for this purpose. Many varieties of temporal logic

have been defined in the past twenty years—we focus on propositional linear time temporal

logic (LTL).

There is an intimate connection between models of LTL formulas and languages of

infinite words—the models of an LTL formula constitute an ω-regular language over an

appropriate alphabet. As a result, the satisfiability problem for LTL reduces to checking

for emptiness of ω-regular languages. This connection was first explicitly pointed out in.

\section{$\omega$-regular languages}

\begin{def:finite words}

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$.

\end{def:finite words}

\begin{def:regular languages}

The class of regular languages is defined recursively over an alphabet $\Sigma$:

\begin{multicols}{2}

\begin{itemize}

\item $\emptyset$ is regular

\item $\{\varepsilon\}$ is regular

\item $\forall_{a \in \Sigma}:\{a\}$ is regular

\end{itemize}

\end{multicols}

\end{def:regular languages}

\begin{def:regular languages closure}

Let $L_{R_1}, L_{R_2} \in \Sigma^*$ be regular. The class of regular languages is closed under following operations:

\begin{multicols}{2}

\begin{itemize}

\item $L_{R_1}^*$

\item $L_{R_1} \circ L_{R_2}$

\item $L_{R_1} \cup L_{R_2}$

\item $L_{R_1} \cap L_{R_2}$

\item $\overline{L}_{R_1}$ and therefore $L_{R_1} - L_{R_2}$

\end{itemize}

\end{multicols}

\end{def:regular languages closure}

\begin{def:infinite words}

$\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$.

\end{def:infinite words}

\begin{def:omega regular languages}

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$.

\end{def:omega regular languages}

\begin{def:omega regular languages closure}

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:

\begin{itemize}

\item $L_R \circ L_{\omega_1}$, but \emph{not} $L_{\omega_1} \circ L_R$

\item $L_{\omega_1} \cup L_{\omega_2}$, but only \emph{finitely} many times

\end{itemize}

\end{def:omega regular languages closure}

\section{B\"uchi automata}

\begin{def:buechi automata}

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$.

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$.

Within this text \emph{automaton} will refer to the non-deterministic B\"uchi automaton, unless otherwise noted. 

\end{def:buechi automata}

\begin{def:automata runs}

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.

\end{def:automata runs}

\begin{def:automata acceptance}

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$.

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$. A language $L$ is \emph{B\"uchi-recognisable} iff there is an automaton $A$ with $L = L_\omega(A)$.

\end{def:automata acceptance}

\subsection{Generalised B\"uchi automata}

\begin{def:general automata}

A \emph{generalised B\"uchi automaton} $A$ is a tuple $(\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$.

\end{def:general automata}

\begin{def:general acceptance}

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$. 

\end{def:general acceptance}

\begin{prop:general equiv}

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:

\[L(A) = \bigcap_{i < k} L(A_i)\]

\end{prop:general equiv}

\noindent Intuitively follows the equivalance of the language recognition abilities of general and non-deterministic B\"uchi automata.

\section{Linear temporal logic}

\subsection{Syntax}

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:

\[\varphi ::= p \in \Prop \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, X \varphi \,|\, \varphi U \varphi\]

\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}

\begin{def:frames}

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 discrete time. 

\end{def:frames}

\begin{def:models}

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)$. 

%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)$.

\end{def:models}

\begin{def:satisfiability}

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$:

\begin{itemize}

\item $\M,i \models p$ for $p \in \Prop$ iff $p \in V(i)$

\item $\M,i \models \neg \varphi$ iff not $\M,i \models \varphi$

\item $\M,i \models \varphi \lor \psi$ iff $\M,i \models \varphi$ or $\M,i \models \psi$

\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 $\Prop$, we define the \emph{vocabulary} $Voc(\varphi)$ of $\varphi$ inductively:

\begin{multicols}{2}

\begin{itemize}

\item $Voc(p) = \{p\}$ for $p \in \Prop$

\item $Voc(\neg \varphi) = Voc(\varphi)$

\item $Voc(\varphi \lor \psi) = Voc(\varphi) \cup Voc(\psi)$

\item $Voc(X \varphi) = Voc(\varphi)$

\item $Voc(\varphi U \psi) = Voc(\varphi) \cup Voc(\psi)$

\end{itemize}

\end{multicols}

%

\noindent Let $\M = (\F, V)$ be a model and $\varphi$ a LTL-formula, we define model $\M_{Voc(\varphi)} = (\F, V_{Voc(\varphi)})$ with:

\[\forall{i \in \N}: V_{Voc(\varphi)}(i) = V(i) \cap Voc(\varphi)\]

Henceforth, we will abbreviate $\M_{Voc(\varphi)}$ and $V_{Voc(\varphi)}$ with $\M_\varphi$ and $V_\varphi$ accordingly. 

%\noindent Let $\M$ be a model and $\varphi$ a LTL-formula, we define model $\M_{Voc(\varphi)}$:

%\[\forall{i \in \N}: \M_{Voc(\varphi)} = \M(i) \cap Voc(\varphi)\]

\end{def:vocabulary}

%

\begin{prop:vocabulary sat}

Let $\M$ be a model and $\varphi$ a LTL-formula, then following holds:

\[\forall{i \in \N}: \M,i \models \varphi \iff \M_\varphi,i \models \varphi\] 

\end{prop:vocabulary sat}

%

\subsection{Derived connectives}

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}. 

Let $\varphi$ and $\psi$ be $L_{LTL}(\Prop)$-formulae:

\begin{multicols}{2}

\begin{itemize}

\item $\top \equiv p \lor \neg p$ for $p \in \Prop$

\item $\bot \equiv \neg \top$

\item $\varphi \land \psi \equiv \neg (\neg \varphi \lor \neg \psi)$

\item $\varphi \rightarrow \psi \equiv \neg \varphi \lor \psi$

\item $\varphi \leftrightarrow \psi \equiv (\varphi \rightarrow \psi) \land (\psi \rightarrow \varphi)$

\item $\Diamond \varphi \equiv \top U \varphi$

\item $\Box \varphi \equiv \neg \Diamond \neg \varphi$

\end{itemize}

\end{multicols}

From the derivations for operators $\Diamond$, \emph{read diamond}, and $\Box$, \emph{read box}, it follows:

\begin{multicols}{2}

\begin{itemize}

\item $\M,i \models \Diamond \varphi$ iff $\exists{k \geq i}: \M,k \models \varphi$

\item $\M,i \models \Box \varphi$ iff $\forall{k \geq i}: \M,k \models \varphi$

\end{itemize}

\end{multicols}

With the additional derived connectives we get the following $L_{LTL}(\Prop)$-formulae productions:

\[\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\]

\section{Automata construction}

Before applying the automata-theoretic verification methods, we need to construct an automaton for a given specification formula $\varphi$. For that, we treat the model $\M = (\F, V)$ for an LTL-formula $\varphi$ as an infinite word over the finite alphabet $2^{Voc(\varphi)}$. We define the infinite word representing the model $\M_\varphi = (\F, V_\varphi)$ by the image of its validation function $V_\varphi^\rightarrow(\N)$.

\[Mod(\varphi) = \{V_\varphi^\rightarrow(\N) \mid \M_\varphi = (\F, V_\varphi) \land \M_\varphi,0 \models \varphi\}\]

$Mod(\varphi)$ is the set of all infinite words, which represent models for $\varphi$.

\section{Model checking}

\section{On-the-fly methods}

\begin{thebibliography}{99}

\bibitem{ref:ltl&büchi} 

\uppercase{M{\footnotesize adhavan} M{\footnotesize ukund}.}

{\em Linear-Time Temporal Logic and B\"uchi Automata}.

Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, 1997.

\bibitem{ref:handbook} 

\uppercase{P{\footnotesize atrick} B{\footnotesize lackburn}, 

F{\footnotesize rank} W{\footnotesize olter and} J{\footnotesize ohan van} B{\footnotesize enthem}.}

{\em Handbook of Modal Logic (Studies in Logic and Practical Reasoning)}.

3rd Edition, Elsevier, Amsterdam, 2007.

\bibitem{ref:alternating verification} 

\uppercase{M{\footnotesize oshe} Y. V{\footnotesize ardi}.}

{\em Alternating Automata and Program Verification}.

Computer Science Today, Volume 1000 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1995.

\bibitem{ref:infpaths}

\uppercase{P{\footnotesize ierre} W{\footnotesize olper}, 

M{\footnotesize oshe} Y. V{\footnotesize ardi and}

A. P{\footnotesize rasad} S{\footnotesize istla}.}

{\em Reasoning about Infinite Computation Paths}.

In Proceedings of the 24th IEEE FOCS, 1983.

\end{thebibliography}

\end{document}