1 \documentclass[a4paper, pagesize, DIV=calc, smallheadings]{article}
3 %\usepackage[latin1]{inputenc}
4 \usepackage{amsmath, amsthm, amssymb}
7 \usepackage{algorithmic}
8 %\usepackage[T1]{fontenc}
12 \renewcommand{\familydefault}{\sfdefault}
13 \title{\uppercase{\textbf{\Large{A}\large{lgorithmic} \Large{V}\large{erification of} \Large{R}\large{eactive} \Large{S}\large{ystems}}\\
17 \uppercase{{\small{E}\scriptsize{UGEN} \small{S}\scriptsize{AWIN}}\\
18 {\em \small{U}\scriptsize{NIVERSITY OF} \small{F}\scriptsize{REIBURG}}\\
19 %{\em \small{C}\scriptsize{omputer} \small{S}\scriptsize{cience} \small{D}\scriptsize{epartment}}\\
20 {\em \small{G}\scriptsize{ERMANY}}}\\
21 %\texttt{\footnotesize{sawine@informatik.uni-freiburg.de}}
23 \date{\textsc{\hfill}}
25 \theoremstyle{definition} %plain, definition, remark
26 \newtheorem*{def:finite words}{Finite words}
27 \newtheorem*{def:infinite words}{Infinite words}
28 \newtheorem*{def:regular languages}{Regular languages}
29 \newtheorem*{def:regular languages closure}{Regular closure}
30 \newtheorem*{def:omega regular languages}{$\omega$-regular languages}
31 \newtheorem*{def:omega regular languages closure}{$\omega$-regular closure}
38 %\renewcommand\abstractname{Abstract}
40 Over the past two decades, temporal logic has become a very basic tool for spec-
41 ifying properties of reactive systems. For finite-state systems, it is possible to use
42 techniques based on B\"uchi automata to verify if a system meets its specifications.
43 This is done by synthesizing an automaton which generates all possible models of
44 the given specification and then verifying if the given system refines this most gen-
45 eral automaton. In these notes, we present a self-contained introduction to the basic
46 techniques used for this automated verification. We also describe some recent space-
47 efficient techniques which work on-the-fly.
51 \section{Introduction}
52 Program verification is a fundamental area of study in computer science. The broad goal
53 is to verify whether a program is ``correct''--i.e., whether the implementation of a program
54 meets its specification. This is, in general, too ambitious a goal and several assumptions
55 have to be made in order to render the problem tractable. In these lectures, we will focus
56 on the verification of finite-state reactive programs. For specifying properties of programs,
57 we use linear time temporal logic.
59 What is a reactive program? The general pattern along which a conventional program
60 executes is the following: it accepts an input, performs some computation, and yields an
61 output. Thus, such a program can be viewed as an abstract function from an input domain
62 to an output domain whose behaviour consists of a transformation from initial states to
65 In contrast, a reactive program is not expected to terminate. As the name suggests, such
66 systems “react” to their environment on a continuous basis, responding appropriately to
67 each input. Examples of such systems include operating systems, schedulers, discrete-event
68 controllers etc. (Often, reactive systems are complex distributed programs, so concurrency
69 also has to be taken into account. We will not stress on this aspect in these lectures—we
70 take the view that a run of a distributed system can be represented as a sequence, by
71 arbitrarily interleaving concurrent actions.)
73 To specify the behaviour of a reactive system, we need a mechanism for talking about
74 the way the system evolves along potentially infinite computations. Temporal logic
75 has become a well-established formalism for this purpose. Many varieties of temporal logic
76 have been defined in the past twenty years—we focus on propositional linear time temporal
79 There is an intimate connection between models of LTL formulas and languages of
80 infinite words—the models of an LTL formula constitute an ω-regular language over an
81 appropriate alphabet. As a result, the satisfiability problem for LTL reduces to checking
82 for emptiness of ω-regular languages. This connection was first explicitly pointed out in.
84 \section{$\omega$-regular languages}
85 \begin{def:finite words}
86 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$.
87 \end{def:finite words}
89 \begin{def:regular languages}
90 The class of regular languages is defined recursively over an alphabet $\Sigma$:
92 \item $\emptyset$ is regular
93 \item $\{\varepsilon\}$ is regular
94 \item $\forall_{a \in \Sigma}:\{a\}$ is regular
96 \end{def:regular languages}
98 \begin{def:regular languages closure}
99 Let $L_{R_1}, L_{R_2} \in \Sigma^*$ be regular. The class of regular languages is closed under following operations:
102 \item $L_{R_1} \circ L_{R_2}$
103 \item $L_{R_1} \cup L_{R_2}$
104 \item $L_{R_1} \cap L_{R_2}$
105 \item $\overline{L}_{R_1}$ and therefore $L_{R_1} - L_{R_2}$
107 \end{def:regular languages closure}
109 \begin{def:infinite words}
110 $\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$, view the word as a function $w : \mathbb{N}_0 \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$.
111 \end{def:infinite words}
113 \begin{def:omega regular languages}
114 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$.
115 \end{def:omega regular languages}
117 \begin{def:omega regular languages closure}
118 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:
120 \item $L_R \circ L_{\omega_1}$, but \emph{not} $L_{\omega_1} \circ L_R$
121 \item $L_{\omega_1} \cup L_{\omega_2}$, but only \emph{finitely} many times
123 \end{def:omega regular languages closure}
126 \section{B\"uchi automata}
128 \section{Linear temporal logic}
130 \section{Model checking}
131 \begin{thebibliography}{99}
132 \bibitem{ref:ltl&büchi}
133 \uppercase{M{\footnotesize adhavan} M{\footnotesize ukund}.}
134 {\em Linear-Time Temporal Logic and B\"uchi Automata}.
135 Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, 1997.
137 \bibitem{ref:handbook}
138 \uppercase{P{\footnotesize atrick} B{\footnotesize lackburn},
139 F{\footnotesize rank} W{\footnotesize olter and} J{\footnotesize ohan van} B{\footnotesize enthem}.}
140 {\em Handbook of Modal Logic (Studies in Logic and Practical Reasoning)}.
141 3rd Edition, Elsevier, Amsterdam, 2007.
143 \bibitem{ref:infpaths}
144 \uppercase{P{\footnotesize ierre} W{\footnotesize olper},
145 M{\footnotesize oshe} Y. V{\footnotesize ardi and}
146 A. P{\footnotesize rasad} S{\footnotesize istla}.}
147 {\em Reasoning about Infinite Computation Paths}.
148 In Proceedings of the 24th IEEE FOCS, 1983.
150 \end{thebibliography}