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

\usetikzlibrary{automata}

%\usepackage{fullpage}

%\usepackage{a4wide}

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

%\usepackage[T1]{fontenc}

%\usepackage{arev}

%\pagestyle{headings}

\floatname{algorithm}{Function}

\renewcommand{\algorithmicrequire}{\textbf{Input:}}

\renewcommand{\algorithmicensure}{\textbf{Output:}}

\renewcommand{\familydefault}{\sfdefault}

\renewenvironment{proof}{{\bfseries Proof.}}{}

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

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

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

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

\newcommand{\A}{\mathcal{A}}

\newcommand{\X}{\mathcal{X}}

\newcommand{\U}{\mathcal{U}}

\newcommand{\V}{\mathcal{V}}

\newcommand{\dnf}{\mathsf{dnf}}

\newcommand{\consq}{\mathsf{consq}}

\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{\texttt{sawine@informatik.uni-freiburg.de}}\\

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

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

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

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

}

\date{\textsc{\hfill}}

\theoremstyle{definition} %plain, definition, remark, proof, corollary

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

\newtheorem*{def:fs closure}{Closure}

\newtheorem*{def:atoms}{Atoms}

\newtheorem*{def:rep function}{Representation function}

\newtheorem*{def:next}{Next function}

\newtheorem*{def:dnf}{Disjunctive normal form}

\newtheorem*{def:positive formulae}{Positive formulae}

\newtheorem*{def:consq}{Logical consequences}

\newtheorem*{def:partial automata}{Partial automata}

\theoremstyle{plain}

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

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

\newtheorem{prop:computation set=language}{Proposition}[section]

\theoremstyle{plain}

\newtheorem{thm:model language}{Theorem}[section]

\newtheorem{cor:mod=model language}{Corollary}[thm:model language]

\newtheorem{cor:mod=program language}[cor:mod=model language]{Corollary}

\newtheorem{thm:model checking}{Theorem}[section]

\newtheorem{lem:dnf}{Lemma}[section]

\newtheorem{lem:consq}[lem:dnf]{Lemma}

\begin{document}

\maketitle

\thispagestyle{empty}

%\itshape

%\renewcommand\abstractname{Abstract} 

\begin{abstract}

Algorithmic verification is an application of automated temporal reasoning based on model checking. Modal logics give us the power to specify system properties. System verification provides a correctness proof for the program design with respect to such properties. We apply methods, which are a composition of automata theory, graph theory and modal logics. This text is an introduction to the automata-theoretic constructions and space-efficient on-the-fly methods for the verification of reactive systems.

\end{abstract}

%\normalfont

\newpage

\section{Introduction}

The rapid digital evolution of semi-conductor design has changed the way of development in the industry. Exponential growth in processing power has massive implications on the complexity of chip-design. When a considerable portion of the development cycle is dedicated to design validation, an increasingly high effort is invested in the realisation of efficient verification methods.

The computer hardware industry has adapted to the rise of complexity by the application of automated design verification. Another natural consequence was the preference of standard, non-specialised hardware solutions accompanied by software implementations of the required functionality. Software systems have penetrated all industries, and increasingly so in high-demand and safety-critical application areas. Software programs e.g. provide high-demand server infrastructures for the Internet, control our air traffic and increase safety in motor traffic. When handling such critical systems, it becomes inevitable to verify the correctness of the software solutions. 

Compared to hardware design, the highly dynamic properties of software components confront us with another state space explosion. Concurrent system designs increase the complexity of verification by some orders of magnitude; and concurrent applications have started to dominate recent software solutions, because we are closing the physical limits for single-core processor frequencies.

Again, the industry is facing a \emph{validation crisis} \cite{ref:automated verification}, and formal verification methods are in high demand. Deductive, computer-supported verification techniques are an interesting digression, but may not be applicable in the validation of software systems of high complexity. Theories for algorithmic verification have existed for decades and recent successful applications have demonstrated their practical value.

In this text, we provide an introduction to formal verification by means of algorithmic methods. Such an algorithmic approach is the base for automated verification procedures. We will concentrate on the validation of reactive programs, without any loss of the general applicability of the presented methods. Reactive systems are, in contrast to terminating programs, continuous processes. Once initiated, a reactive system persists in an active state, where it reacts to concurrent inputs with appropriate actions. Examples of reactive systems are monitoring processes, schedulers and even whole operating systems.

The first three sections define the preliminaries for the automata-theoretic constructions. At first, we provide the notion of reasoning about infinite computational paths within formal language theory. Then we tackle those infinite structures with the help of automata theory, which builds the framework of the formal verification theory. Next we introduce the reader to modal logics, in particular to linear temporal logic. Linear temporal logic is the language we use to talk about system properties, i.e., the system specification language. 

The fifth section interweaves automata theory and modal logics for the formalisation of the automata constructions, i.e., we construct automata depicting the program design and the specified properties. Based on this constructions, we apply the methods presented in the model checking section. The last section is a short excursion into the practical considerations of automated verification. For a successful application of automated verification, we consider ways of reducing the complexity of the automata-theoretic approach.

The formal frame of this text is mostly based on Madhavan Mukund's \cite{ref:ltl&büchi} and Moshe Y. Vardi's \cite[C.17]{ref:handbook} work. We conclude this paper with a discussion of \cite{ref:ltl&büchi}.

\section{$\omega$-regular languages}

For the formalisation of non-terminating, reactive systems, we need to get familiar with the concept of infinity. When a system is persistently active, the conceptual model of its input becomes an infinite structure, and likewise the description of its computational path. We want to settle this infinite structures within a formal corset.

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

Automata theory is the foundation of state-based modelling of computation. Non-deter\-ministic automata provide an elegant way of describing interleaving systems. B\"uchi automata extend the idea of such automata to comfort the need for computational models on infinite inputs.

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

With infinite inputs comes a new definition of acceptance. Automata on finite inputs define acceptance by the termination of the computation in an accepting state. This notion needs adjustments, when modelling non-terminating systems. First, we need to define the legal sequence of state transitions of an automaton when reading an infinite input word.

\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 occurrences, 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)$. The class of B\"uchi-recognisable languages corresponds to the class of $\omega$-regular languages.

\end{def:automata acceptance}

Given all legal computations of an automaton, we have defined the acceptance condition. A computation is accepting, if it passes through an accepting state infinitely times. Since the set of states $S$ is finite, there must be a state $s \in S$, which occurs infinitely often within an infinite run; but it is not necessary, that $s$ is an accepting state; notice that $F$ can be an empty set.

\subsection{Example}

Let $\A_1 = (\Sigma, S, S_0, \Delta, F)$ be an automaton.

\begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto]

\draw[help lines] (0,0) grid (3,2);

\node[state,initial] (q_0) {$q_0$};

\node[state] (q_1) [above right of= q_0] {$q_1$};

\node[state] (q_2) [below right of= q_0] {$q_2$};

\node[state,accepting](q_3) [below right of= q_1] {$q_3$};

\path[->] (q_0) edge node {0} (q_1)

edge node [swap] {1} (q_2)

(q_1) edge node {1} (q_3)

edge [loop above] node {0} ()

(q_2) edge node [swap] {0} (q_3)

edge [loop below] node {1} ();

\end{tikzpicture}

\subsection{Generalised B\"uchi automata}

In the following two sections, we present the modal logic, which is used for the specification of system properties and automata construction on such specifications. To provide a more convenient link between linear temporal logic and B\"uchi automata, we introduce a slightly different formalisation of automata with an extended acceptance condition.

\begin{def:general automata}

A \emph{generalised B\"uchi automaton} is a tuple $\A = (\Sigma, S, S_0, \Delta, \{F_i\}_{i < k})$ for $i \in \N$, where the \emph{accepting 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 equivalence condition holds:

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

\end{prop:general equiv}

\noindent The equivalence of the language recognition abilities of general and non-deterministic B\"uchi automata follows intuitively.

\section{Linear temporal logic}

%All arts and sciences interpret time in some way: historians prefer the past tense, while politicians make only promises for the future.

Nothing escapes time, but time has successfully escaped its capture in computer science until the rise of the modal logics in the second half of the 20th century \cite[C.11]{ref:handbook}. Physicists know many time arrows, one of which constitutes the thermodynamic arrow of time, which happens to be the one we perceive by remembering the past and not the future. We compensate our inability to control the direction of time by the use of rigorous language constructs when reasoning about temporal events.

When natural language fails in providing unambiguousness, we have to resort to formal languages. To handle discrete time, we use \emph{propositional logic} as the base and extend it by some more or less modal connectives. There are two major temporal logics used in the specification of system properties, \emph{linear temporal logic}, short LTL, and \emph{branching temporal logic}, short CTL -- for computation tree logic. Throughout this text, we will restrict our attention to 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\]

%

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

\subsection{Semantics}

Temporal logics are interpreted over computation paths; in LTL such a path depicts a linear sequence, where in CTL the path is a tree with branching connectives. In the interpretation of LTL over \emph{computation paths}, a computation corresponds to a model over a \emph{Kripke-frame} constructed by the order of natural numbers.

\begin{def:frames}

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. 

\end{def:frames}

%

\noindent The frame defines the structure of linear time and the flow temporal events. To perfect our structure for temporal reasoning, we need to give those events a formal meaning. We do so by assigning a value to each atomic proposition.

\begin{def:models}

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

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

%

\noindent From the strict linear order of the LTL-frame accessibility relation follows that an LTL-formula $\varphi$ is \emph{satisfiable}, iff there exists a model $\M$ with $\M,0 \models \varphi$.

We clearly see, that atomic propositions, which are not contained within the formula $\varphi$ are redundant to the the definition of the satisfiability. By defining the \emph{vocabulary} of a formula, we dispose such irrelevant atomic proposition from the alphabet.

\begin{def:vocabulary}

Let $\varphi$ be an 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$ an 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$ an 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$ an 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}

\label{sec: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}. 

In anticipation of section \ref{sec:on-the-fly methods}, we extend our logic's syntax with the binary connective $\V$, the dual of $\U$, which will become useful in the interpretation known as the \emph{two-state semantics}.

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$

\item $\varphi \V \psi \equiv \neg(\neg \varphi \U \neg \psi)$

\end{itemize}

\end{multicols}

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

\noindent 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 the automaton for a given specification formula $\varphi$ and for the program $P$ in test.

\subsection{Specification automata}

\label{sec:specification automata}

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

\begin{def:rep function}

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

\[Mod(\varphi) = \{rep(\M_\varphi) \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$.

\end{def:rep function}

\begin{def:fs closure}

\label{def:fs closure}

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:

%\begin{multicols}{2}

\begin{itemize}

\begin{multicols}{2}

\item $\varphi \in CL(\varphi)$

\item $\neg \psi \in CL(\varphi) \implies \psi \in CL(\varphi)$

\item $\psi \in CL(\varphi) \implies \neg \psi \in CL(\varphi)$

\item $\psi \lor \chi \in CL(\varphi) \implies \psi, \chi \in CL(\varphi)$

\item $\X \psi \in CL(\varphi) \implies \psi \in CL(\varphi)$

\item $\psi \V \chi \in CL(\varphi) \implies \psi, \chi \in CL(\varphi)$

\end{multicols}

\vspace{-1.1em}

\item $\psi \U \chi \in CL(\varphi) \implies \psi, \chi, \X(\psi \U \chi) \in CL(\varphi)$

\end{itemize}

%\end{multicols}

\end{def:fs closure}

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

\[\mathbb{U}_\varphi = \{\psi \U \chi \mid \psi \U \chi \in CL(\varphi)\} \text{ and } \mathbb{U}_{\varphi_i} \text{ denotes the $i^{th}$ element of } \mathbb{U_\varphi}\]

\begin{def:atoms}

Let $\varphi$ be a formula and $CL(\varphi)$ its closure. $A \subseteq CL(\varphi)$ is an \emph{atom} if following holds:

\begin{itemize}

\item $\forall{\psi \in CL(\varphi)}: \psi \in A \iff \neg \psi \notin A$

\item $\forall{\psi \lor \chi \in CL(\varphi)}: \psi \lor \chi \in A \iff \psi \in A$ or $\chi \in A$ 

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

\end{itemize}

We define the set of all atoms of formula $\varphi$ with $\mathbb{AT}_\varphi = \{A \subseteq CL({\varphi}) \mid A \text{ is an atom}\}$.

\end{def:atoms}

\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\})$ with:

\begin{itemize}

\item $\Sigma = 2^{Voc(\varphi)}$

\item $S = \mathbb{AT_\varphi}$

\item $S_0 = \{A \in \mathbb{AT_\varphi} \mid \varphi \in A\}$

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

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

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

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

%Let $A, B \in \mathbb{AT}$ and $P \subseteq Voc(\varphi)$. Then $(A, P, B) \in \Delta$ iff the following holds:

%$P = A \cap Voc(\varphi)$ and For all $\X \psi \in CL(\varphi): \X \psi \in A$ iff $\psi \in B$.

\end{itemize}

\begin{thm:model language}

\label{thm:model language}

Let $\M_\varphi = (\F, V_\varphi)$ be a model and $rep(\M_\varphi)$ its infinite representation word, then following holds:

\[rep(\M_\varphi) \in L_\omega(\A_\varphi) \iff \M_\varphi,0 \models \varphi\]

\end{thm:model language}

\noindent

\begin{proof}

For the elaborate proof, consult \cite{ref:ltl&büchi}.

\end{proof}

\begin{cor:mod=model language}

\label{cor:mod=model language}

From Theorem \ref{thm:model language} follows $Mod(\varphi) = L_\omega(\A_\varphi)$.

\end{cor:mod=model language}

\subsection{Program automata}

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

We construct automaton $\A_P = (\Sigma, S, S_0, \Delta, F)$, with:

\begin{itemize}

\begin{multicols}{2}

\item $\Sigma = 2^\Prop$

\item $S = S_P$

\item $S_0 = \{s_0\}$

\item $F = S$

\end{multicols}

\vspace{-1.1em}

\item $\Delta = \{(s, V(s), s') \mid \exists{a \in \Prop}: (s, a, s') \in R\}$

\end{itemize}

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

\begin{prop:computation set=language}

\label{prop:computation set=language}

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

\[L_\omega(\A_P) = \{\rho \mid \rho \text{ is a run of } \A_P\}\]

\end{prop:computation set=language}

 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:

\[Mod(P) = \{\rho \mid \rho \text{ is a computation of } P\}\]

\begin{cor:mod=program language}

\label{cor:mod=program language}

From Theorem \ref{thm:model language} and Proposition \ref{prop:computation set=language} follows $Mod(P) = L_\omega(\A_P)$.

\end{cor:mod=program language}

\section{Model checking}

For effective automata-theoretic verification of reactive programs, we have modeled the program as a non-deterministic B\"uchi automaton $\A_P$ and the specification formula $\varphi$ as automaton $\A_\varphi$. 

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

In conclusion, the essence of model checking lies within the test for emptiness of the intersection between the recognised language of the program automaton and the recognised language of the automaton for its negated specification:

\[L_\omega(\A_P) \cap L_\omega(\A_{\neg \varphi}) = \emptyset\]

\begin{thm:model checking}

\label{thm:model checking}

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

\end{thm:model checking}

\noindent From Corollary \ref{cor:mod=model language} and \ref{cor:mod=program language} follows:

\[L_\omega(\A_P) \cap L_\omega(\A_{\neg \varphi}) = \emptyset \iff Mod(P) \cap Mod(\neg \varphi) = \emptyset\]

\subsection{Complexity}

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 asymptotic complexity of the presented automata-theoretic verification method is in time $O(|P| \cdot 2^{O(|\varphi|)})$ \cite{ref:concurrent checking}. 

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: despite that the upper bound is polynomial in the size of the program, in practice, we are facing exponential growth in complexity \cite[C.17]{ref:handbook}.

\section{On-the-fly methods}

\label{sec:on-the-fly methods}

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 emptiness test. 

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.

\subsection{Two-state semantics}

A new interpretation for the infinite computation paths will help us in the incremental construction of automata. We separate the computation paths in two states by applying temporal reasoning; and we do so incrementally for each time instant. The two states resemble the satisfiability requirements for any time instant $i$ and its successor $i+1$.

\subsubsection{Example}

Let $\varphi = a \U b$. We apply the two-state semantics on $\varphi$ and it follows:

\[\forall{i \in \N}: \M,i \models \varphi \iff \M,i \models b \text{ or } \M,i+1 \models a \land \X(\varphi)\]

In this example, we construct the specification automaton incrementally for each time instant; the states are constructed from the union of the current-state and next-state requirements $\{b\} \cup \{a, \X(\varphi)\}$.

Let us formalise the notion of the incremental automaton construction based on the idea of the two-state semantics.

\begin{def:positive formulae}

Let $\Prop$ be a set of atomic propositions and let $\overline{\Prop} = \{\neg p \mid p \in \Prop\}$. We define the set of LTL-formulae in \emph{positive form}:

\[\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^+\} \]

\end{def:positive formulae}

The positive form of a formula contains only negations at the level of atomic propositions. This is the reason for the introduction of the dual $\V$ in \ref{sec:derived connectives}; to provide a way of shifting the negation of $\U$-formulae inwards by the substitution with its contra-positive form. 

\begin{def:next}

Let $\Phi$ be a set of LTL-formulae, we define:

\[next(\Phi) = \{ \X\varphi \mid \X\varphi \in \Phi\} \text{ and } snext(\Phi) = \{ \varphi \mid \X\varphi \in \Phi\}\]

\end{def:next}

\begin{def:dnf}

Let $\Phi^+$ be the set of LTL-formulae in positive form and let $Q = \Prop \cup \overline{\Prop} \cup next(\Phi^+)$. We define the function $\dnf: \Phi^+ \to 2^Q$ inductively:

\begin{align*}

&\dnf(\top) &=  &\, \{\emptyset\}\\

&\dnf(\bot) &= &\, \emptyset\\

&\dnf(x) &=  &\, \{\{x\}\}, \text{ for } x = p, \neg p, \X\varphi\\

&\dnf(\varphi \lor \psi) &=  &\, \dnf(\varphi) \cup \dnf(\psi)\\

&\dnf(\varphi \land \psi) &=  &\, \{C \cup D \mid C \in \dnf(\varphi), D \in \dnf(\psi), C \cup D \text{ is consistent}\}\\

&\dnf(\varphi \U \psi) &=  &\, \dnf(\varphi \land \X(\varphi \U \psi)) \cup \dnf(\psi)\\

&\dnf(\varphi \V \psi) &=  &\, \dnf(\varphi \land \psi) \cup \dnf(\psi \land \X(\varphi \V \psi))

\end{align*}

\end{def:dnf}

\noindent The disjunctive normal form provides the partitioning for the automata state construction over the two-state semantics. The modal connectives $\U$ and $\V$ are interpreted as disjunctions over the path of computation.

\begin{lem:dnf}

Let $\Phi^+$ be the set of formulae in positive form and let $\M_\varphi$ be a model over the vocabulary of $\varphi$ then following holds:

\[\forall{\varphi \in \Phi^+}: \M_\varphi,0 \models \varphi \iff \M_\varphi,0 \models \bigvee_{D \in \dnf(\varphi)} \bigwedge D\]

\end{lem:dnf}

\begin{def:consq}

Let $C \subseteq CL(\varphi)$, then $\consq(C)$ is the smallest subset of $CL(\varphi)$ such that following holds:

\begin{itemize}

%\begin{tabular}{ll}

\begin{multicols}{2}

\item $C \subseteq \consq(C)$

\item $\top \in \consq(C)$, if $\top \in CL(\varphi)$

\end{multicols}

\vspace{-1em}

\item $\psi \lor \chi \in \consq(C)$, if $\psi \lor \chi \in CL(\varphi)$ and $\psi \in \consq(C) \lor \chi \in \consq(C)$

\item $\psi \land \chi \in \consq(C)$, if $\psi \land \chi \in CL(\varphi)$ and $\psi, \chi \in \consq(C)$

\item $\psi \U \chi \in \consq(C)$, if $\psi \U \chi \in CL(\varphi)$ and $\psi, \X(\psi \U \chi) \in \consq(C) \lor \chi \in \consq(C)$

\item $\psi \V \chi \in \consq(C)$, if $\psi \V \chi \in CL(\varphi)$ and $\psi, \X(\psi \U \chi) \in \consq(C) \lor \psi, \chi \in \consq(C)$

%\end{tabular}

\end{itemize}

\end{def:consq}

\begin{lem:consq}

Let $\psi \in CL(\varphi)$, let $C, D \subseteq CL(\varphi)$ and let $\M$ be a model, then following holds:

\begin{itemize}

\begin{multicols}{2}

\item $\consq(C) \subseteq \consq(D)$, if $C \subseteq D$

\item $\psi \in \consq(C)$, if $C \in \dnf(\psi)$

\item $\psi \in \consq(D)$, if $\psi \in C \land D \in \dnf(\bigwedge C)$

\item $\M,0 \models \bigwedge \consq(C)$, if $\M,0 \models \bigwedge C$

\end{multicols}

\end{itemize}

\end{lem:consq}

\begin{def:partial automata}

Let $\varphi$ be a formula with its disjunctive normal form $\dnf(\varphi)$ and let $Q = \Prop \cup \overline{\Prop} \cup next(CL(\varphi))$. Again we use the subset $\mathbb{U}_\varphi \subseteq CL(\varphi)$ of \emph{until}-formulae of the closure as defined in \ref{def:fs closure}. We define the \emph{partial automaton} $\A_\varphi = (\Sigma, S, S_0, \Delta, \{F_i\})$ with:

\begin{itemize}

\item $\Sigma = 2^{Voc(\varphi)}$

\item $S = 2^Q$

\item $S_0 = \dnf(\varphi)$

\item $\Delta = \{(A, P, B) \mid \A \cap \Prop \subseteq P$ and $\{p \mid \neg p \in A\} \cap P = \emptyset$ and $B \in \dnf(\bigwedge snext(A)) \}$

\item $F_i = \{A \in S \mid \psi \U \chi = \mathbb{U}_{\varphi_i}$ and $\psi \U \chi \notin \consq(A) \lor \chi \in \consq(A) \}$

\end{itemize}

\end{def:partial automata}

\noindent The soundness and completeness proofs are provided in \cite{ref:ltl&büchi}; the equivalence of the partial automata and the specification automata as defined in \ref{sec:specification automata} follows from the proofs.  

\subsection{On-the-fly construction}

The sequential description of the program design makes it trivial to incrementally construct the program automaton state by state. The more difficult part is the construction of the partial specification automaton on-the-fly. 

To archive this, we begin with a set of states built by applying $\dnf(\varphi)$. In the next step we determine a state within the current set of states, which is consistent with the program automaton. We use this state to expand its successor states. Now, we analyse the expanded state space for cycles. If no cycles are detected, we repeat this procedure, while there are still consistent states left. 

When the procedure terminates, we check whether the specification automaton was fully built. If that is the case, we have explored the whole state space of both automata and have not found any cycles, i.e., the program does satisfy the specification. Otherwise, the procedure was prematurely aborted by a cycle detection, i.e., the program does satisfy the \emph{negated} specification and therefore does \emph{not} meet the specification properties. 

\begin{algorithm}

\caption{expand: $\Phi^+ \times 2^Q \to 2^Q$}

\label{alg:expand}

\begin{algorithmic}

\REQUIRE $Node : node, NodeSet: set\, of\, nodes$

\STATE $ExpandedNodes = \dnf(\bigwedge snext(Node)) - NodeSet$

\RETURN $ExpandedNodes$

\end{algorithmic}

\end{algorithm}

\begin{algorithm}

\caption{verify: $\A \times L_{LTL}(\Prop) \to Boolean$}

\label{alg:create}

\begin{algorithmic}

\REQUIRE $\A_P: automaton, \varphi: formula$

\STATE $S = \dnf(\varphi)$

%\WHILE {$Mod(\bigvee_{s \in S} \bigwedge s) \cap Mod(\A_P) = \emptyset$}

\WHILE {$consistent(S, \A_P) \neq \emptyset \land \neg cycle(S, \A_P)$}

\STATE $Node \in consistent(S, \A_P)$

\STATE $S = S \cup expand(Node, S)$

\ENDWHILE

\RETURN $\neg complete(S, \varphi)$

\end{algorithmic}

\end{algorithm}

\section*{Discussion}

\emph{Linear-Time Temporal Logic and B\"uchi Automata} \cite{ref:ltl&büchi} is an in-depth introduction to automated verification. It delivers the core concepts of model checking in a comprehensible way. The formal proofs are clean and well absorbable. The referenced material effectively fills the gaps, when looking for more detailed explanations, e.g. about the on-the-fly method. Some few, but good examples support the substantiation of the theoretic material. The introduction section provides a good overview of the text structure and the basic theory behind most concepts used. 

However, the author does not make an effort to deliver a motivation for the topic. From the beginning, the substance of the text resides within the context of model checking. Without an external view on the practical applications, the significance of formal verification to the industry remains unclear.

A few definitions are either lacking formality or are inconsistent. It seems like several concepts are introduced ad-hoc and without rigor. In an introductory text, such inaccuracies may lead to confusion and divert the reader's attention from the essence of the presented topic.

\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: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:automated verification} 

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

{\em Automated Verification: Graphs, Logic and Automata}.

Proceeding of the International Joint Conference on Artificial Intelligence, Acapulco, 2003.

\bibitem{ref:on-the-fly verification} 

\uppercase{R{\footnotesize ob} G{\footnotesize erth,}  D{\footnotesize oron} P{\footnotesize eled,} M{\footnotesize oshe} Y. V{\footnotesize ardi and} P{\footnotesize ierre} W{\footnotesize olper}.}

{\em Simple On-the-fly Automatic Verification of Linear Temporal Logic}.

Proceeding IFIO/WG6.1 Symposium on Protocol Specification, Testing and Verification, Warsaw, 1995.

\bibitem{ref:concurrent checking}

\uppercase{O{\footnotesize rna} L{\footnotesize ichtenstein and} A{\footnotesize mir} P{\footnotesize nueli}.}

{\em Checking that finite state concurrent programs satisfy their linear specification}.

Proceeding 12th ACM Symposium on Principles of Programming Languages, New York, 1985.

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

Proceedings of the 24th IEEE FOCS, 1983.

\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, Chapter 11 P. 655-720 and Chapter 17 P. 975-989, 2007.

\end{thebibliography}

\end{document}