sawine@7
|
1 |
\documentclass[a4paper, pagesize, DIV=calc, smallheadings]{article}
|
sawine@2
|
2 |
\usepackage{graphicx}
|
sawine@2
|
3 |
%\usepackage[latin1]{inputenc}
|
sawine@14
|
4 |
\usepackage{amsmath, amsthm, amssymb, amsfonts, verbatim}
|
sawine@2
|
5 |
\usepackage{typearea}
|
sawine@2
|
6 |
\usepackage{algorithm}
|
sawine@2
|
7 |
\usepackage{algorithmic}
|
sawine@15
|
8 |
\usepackage{multicol}
|
sawine@11
|
9 |
%\usepackage{fullpage}
|
sawine@19
|
10 |
%\usepackage{a4wide}
|
sawine@19
|
11 |
\usepackage[left=3.9cm, right=3.9cm]{geometry}
|
sawine@5
|
12 |
%\usepackage[T1]{fontenc}
|
sawine@5
|
13 |
%\usepackage{arev}
|
sawine@7
|
14 |
%\pagestyle{headings}
|
sawine@19
|
15 |
|
sawine@2
|
16 |
\renewcommand{\familydefault}{\sfdefault}
|
sawine@22
|
17 |
\renewenvironment{proof}{{\bfseries Proof.}}{}
|
sawine@17
|
18 |
\newcommand{\M}{\mathcal{M}}
|
sawine@17
|
19 |
\newcommand{\N}{\mathbb{N}_0}
|
sawine@19
|
20 |
\newcommand{\F}{\mathcal{F}}
|
sawine@19
|
21 |
\newcommand{\Prop}{\mathcal{P}}
|
sawine@22
|
22 |
\newcommand{\A}{\mathcal{A}}
|
sawine@19
|
23 |
|
sawine@7
|
24 |
\title{\uppercase{\textbf{\Large{A}\large{lgorithmic} \Large{V}\large{erification of} \Large{R}\large{eactive} \Large{S}\large{ystems}}\\
|
sawine@7
|
25 |
\tiny{Draft}
|
sawine@7
|
26 |
}}
|
sawine@7
|
27 |
\author{
|
sawine@19
|
28 |
\uppercase{{\small{E}\scriptsize{UGEN} \small{S}\scriptsize{AWIN}}\thanks{\lowercase{\scriptsize{\texttt{sawine@informatik.uni-freiburg.de}}}}\\
|
sawine@19
|
29 |
{\em \small{U}\scriptsize{NIVERSITY OF} \small{F}\scriptsize{REIBURG}}\thanks{\tiny{Computer Science Department, Research Group for Foundations of Artificial Intelligence}}\\
|
sawine@7
|
30 |
%{\em \small{C}\scriptsize{omputer} \small{S}\scriptsize{cience} \small{D}\scriptsize{epartment}}\\
|
sawine@7
|
31 |
{\em \small{G}\scriptsize{ERMANY}}}\\
|
sawine@7
|
32 |
%\texttt{\footnotesize{sawine@informatik.uni-freiburg.de}}
|
sawine@7
|
33 |
}
|
sawine@5
|
34 |
\date{\textsc{\hfill}}
|
sawine@7
|
35 |
|
sawine@22
|
36 |
\theoremstyle{definition} %plain, definition, remark, proof, corrolary
|
sawine@7
|
37 |
\newtheorem*{def:finite words}{Finite words}
|
sawine@7
|
38 |
\newtheorem*{def:infinite words}{Infinite words}
|
sawine@8
|
39 |
\newtheorem*{def:regular languages}{Regular languages}
|
sawine@8
|
40 |
\newtheorem*{def:regular languages closure}{Regular closure}
|
sawine@7
|
41 |
\newtheorem*{def:omega regular languages}{$\omega$-regular languages}
|
sawine@8
|
42 |
\newtheorem*{def:omega regular languages closure}{$\omega$-regular closure}
|
sawine@11
|
43 |
\newtheorem*{def:buechi automata}{Automata}
|
sawine@11
|
44 |
\newtheorem*{def:automata runs}{Runs}
|
sawine@11
|
45 |
\newtheorem*{def:automata acceptance}{Acceptance}
|
sawine@21
|
46 |
\newtheorem*{def:general automata}{Generalised automata}
|
sawine@21
|
47 |
\newtheorem*{def:general acceptance}{Acceptance}
|
sawine@14
|
48 |
\newtheorem*{def:vocabulary}{Vocabulary}
|
sawine@19
|
49 |
\newtheorem*{def:frames}{Frames}
|
sawine@18
|
50 |
\newtheorem*{def:models}{Models}
|
sawine@18
|
51 |
\newtheorem*{def:satisfiability}{Satisfiability}
|
sawine@22
|
52 |
\newtheorem*{def:fs closure}{Fischer-Ladner closure}
|
sawine@22
|
53 |
\newtheorem*{def:atoms}{Atoms}
|
sawine@14
|
54 |
|
sawine@22
|
55 |
\theoremstyle{plain}
|
sawine@21
|
56 |
\newtheorem{prop:vocabulary sat}{Proposition}[section]
|
sawine@21
|
57 |
\newtheorem{prop:general equiv}{Proposition}[section]
|
sawine@15
|
58 |
|
sawine@22
|
59 |
\theoremstyle{plain}
|
sawine@22
|
60 |
\newtheorem{thm:model language}{Theorem}[section]
|
sawine@22
|
61 |
|
sawine@0
|
62 |
\begin{document}
|
sawine@0
|
63 |
\maketitle
|
sawine@4
|
64 |
\thispagestyle{empty}
|
sawine@2
|
65 |
%\itshape
|
sawine@2
|
66 |
%\renewcommand\abstractname{Abstract}
|
sawine@0
|
67 |
\begin{abstract}
|
sawine@0
|
68 |
Over the past two decades, temporal logic has become a very basic tool for spec-
|
sawine@0
|
69 |
ifying properties of reactive systems. For finite-state systems, it is possible to use
|
sawine@0
|
70 |
techniques based on B\"uchi automata to verify if a system meets its specifications.
|
sawine@0
|
71 |
This is done by synthesizing an automaton which generates all possible models of
|
sawine@0
|
72 |
the given specification and then verifying if the given system refines this most gen-
|
sawine@0
|
73 |
eral automaton. In these notes, we present a self-contained introduction to the basic
|
sawine@0
|
74 |
techniques used for this automated verification. We also describe some recent space-
|
sawine@0
|
75 |
efficient techniques which work on-the-fly.
|
sawine@0
|
76 |
\end{abstract}
|
sawine@2
|
77 |
%\normalfont
|
sawine@4
|
78 |
\newpage
|
sawine@2
|
79 |
\section{Introduction}
|
sawine@2
|
80 |
Program verification is a fundamental area of study in computer science. The broad goal
|
sawine@5
|
81 |
is to verify whether a program is ``correct''--i.e., whether the implementation of a program
|
sawine@2
|
82 |
meets its specification. This is, in general, too ambitious a goal and several assumptions
|
sawine@2
|
83 |
have to be made in order to render the problem tractable. In these lectures, we will focus
|
sawine@2
|
84 |
on the verification of finite-state reactive programs. For specifying properties of programs,
|
sawine@2
|
85 |
we use linear time temporal logic.
|
sawine@2
|
86 |
|
sawine@2
|
87 |
What is a reactive program? The general pattern along which a conventional program
|
sawine@2
|
88 |
executes is the following: it accepts an input, performs some computation, and yields an
|
sawine@2
|
89 |
output. Thus, such a program can be viewed as an abstract function from an input domain
|
sawine@2
|
90 |
to an output domain whose behaviour consists of a transformation from initial states to
|
sawine@2
|
91 |
final states.
|
sawine@2
|
92 |
|
sawine@2
|
93 |
In contrast, a reactive program is not expected to terminate. As the name suggests, such
|
sawine@2
|
94 |
systems “react” to their environment on a continuous basis, responding appropriately to
|
sawine@2
|
95 |
each input. Examples of such systems include operating systems, schedulers, discrete-event
|
sawine@2
|
96 |
controllers etc. (Often, reactive systems are complex distributed programs, so concurrency
|
sawine@2
|
97 |
also has to be taken into account. We will not stress on this aspect in these lectures—we
|
sawine@2
|
98 |
take the view that a run of a distributed system can be represented as a sequence, by
|
sawine@2
|
99 |
arbitrarily interleaving concurrent actions.)
|
sawine@2
|
100 |
|
sawine@2
|
101 |
To specify the behaviour of a reactive system, we need a mechanism for talking about
|
sawine@2
|
102 |
the way the system evolves along potentially infinite computations. Temporal logic
|
sawine@2
|
103 |
has become a well-established formalism for this purpose. Many varieties of temporal logic
|
sawine@2
|
104 |
have been defined in the past twenty years—we focus on propositional linear time temporal
|
sawine@2
|
105 |
logic (LTL).
|
sawine@2
|
106 |
|
sawine@2
|
107 |
There is an intimate connection between models of LTL formulas and languages of
|
sawine@2
|
108 |
infinite words—the models of an LTL formula constitute an ω-regular language over an
|
sawine@2
|
109 |
appropriate alphabet. As a result, the satisfiability problem for LTL reduces to checking
|
sawine@2
|
110 |
for emptiness of ω-regular languages. This connection was first explicitly pointed out in.
|
sawine@2
|
111 |
|
sawine@8
|
112 |
\section{$\omega$-regular languages}
|
sawine@7
|
113 |
\begin{def:finite words}
|
sawine@11
|
114 |
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
|
115 |
\end{def:finite words}
|
sawine@7
|
116 |
|
sawine@8
|
117 |
\begin{def:regular languages}
|
sawine@8
|
118 |
The class of regular languages is defined recursively over an alphabet $\Sigma$:
|
sawine@15
|
119 |
\begin{multicols}{2}
|
sawine@8
|
120 |
\begin{itemize}
|
sawine@8
|
121 |
\item $\emptyset$ is regular
|
sawine@8
|
122 |
\item $\{\varepsilon\}$ is regular
|
sawine@8
|
123 |
\item $\forall_{a \in \Sigma}:\{a\}$ is regular
|
sawine@8
|
124 |
\end{itemize}
|
sawine@15
|
125 |
\end{multicols}
|
sawine@8
|
126 |
\end{def:regular languages}
|
sawine@8
|
127 |
|
sawine@8
|
128 |
\begin{def:regular languages closure}
|
sawine@10
|
129 |
Let $L_{R_1}, L_{R_2} \in \Sigma^*$ be regular. The class of regular languages is closed under following operations:
|
sawine@15
|
130 |
\begin{multicols}{2}
|
sawine@8
|
131 |
\begin{itemize}
|
sawine@8
|
132 |
\item $L_{R_1}^*$
|
sawine@8
|
133 |
\item $L_{R_1} \circ L_{R_2}$
|
sawine@8
|
134 |
\item $L_{R_1} \cup L_{R_2}$
|
sawine@10
|
135 |
\item $L_{R_1} \cap L_{R_2}$
|
sawine@10
|
136 |
\item $\overline{L}_{R_1}$ and therefore $L_{R_1} - L_{R_2}$
|
sawine@8
|
137 |
\end{itemize}
|
sawine@15
|
138 |
\end{multicols}
|
sawine@8
|
139 |
\end{def:regular languages closure}
|
sawine@8
|
140 |
|
sawine@9
|
141 |
\begin{def:infinite words}
|
sawine@17
|
142 |
$\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
|
143 |
\end{def:infinite words}
|
sawine@9
|
144 |
|
sawine@7
|
145 |
\begin{def:omega regular languages}
|
sawine@8
|
146 |
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
|
147 |
\end{def:omega regular languages}
|
sawine@7
|
148 |
|
sawine@8
|
149 |
\begin{def:omega regular languages closure}
|
sawine@8
|
150 |
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
|
151 |
\begin{itemize}
|
sawine@8
|
152 |
\item $L_R \circ L_{\omega_1}$, but \emph{not} $L_{\omega_1} \circ L_R$
|
sawine@8
|
153 |
\item $L_{\omega_1} \cup L_{\omega_2}$, but only \emph{finitely} many times
|
sawine@8
|
154 |
\end{itemize}
|
sawine@8
|
155 |
\end{def:omega regular languages closure}
|
sawine@7
|
156 |
|
sawine@8
|
157 |
\section{B\"uchi automata}
|
sawine@11
|
158 |
\begin{def:buechi automata}
|
sawine@22
|
159 |
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
|
160 |
|
sawine@22
|
161 |
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
|
162 |
|
sawine@19
|
163 |
Within this text \emph{automaton} will refer to the non-deterministic B\"uchi automaton, unless otherwise noted.
|
sawine@11
|
164 |
\end{def:buechi automata}
|
sawine@11
|
165 |
|
sawine@11
|
166 |
\begin{def:automata runs}
|
sawine@22
|
167 |
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
|
168 |
\end{def:automata runs}
|
sawine@11
|
169 |
|
sawine@11
|
170 |
\begin{def:automata acceptance}
|
sawine@22
|
171 |
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
|
172 |
|
sawine@22
|
173 |
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
|
174 |
|
sawine@22
|
175 |
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
|
176 |
\end{def:automata acceptance}
|
sawine@11
|
177 |
|
sawine@21
|
178 |
\subsection{Generalised B\"uchi automata}
|
sawine@21
|
179 |
\begin{def:general automata}
|
sawine@22
|
180 |
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
|
181 |
\end{def:general automata}
|
sawine@21
|
182 |
|
sawine@21
|
183 |
\begin{def:general acceptance}
|
sawine@22
|
184 |
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
|
185 |
\end{def:general acceptance}
|
sawine@21
|
186 |
|
sawine@21
|
187 |
\begin{prop:general equiv}
|
sawine@22
|
188 |
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@22
|
189 |
\[L(\A) = \bigcap_{i < k} L(\A_i)\]
|
sawine@21
|
190 |
\end{prop:general equiv}
|
sawine@21
|
191 |
\noindent Intuitively follows the equivalance of the language recognition abilities of general and non-deterministic B\"uchi automata.
|
sawine@21
|
192 |
|
sawine@8
|
193 |
\section{Linear temporal logic}
|
sawine@19
|
194 |
\subsection{Syntax}
|
sawine@19
|
195 |
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
|
196 |
\[\varphi ::= p \in \Prop \,|\, \neg \varphi \,|\, \varphi \lor \varphi \,|\, X \varphi \,|\, \varphi U \varphi\]
|
sawine@13
|
197 |
|
sawine@18
|
198 |
\subsection{Interpretation}
|
sawine@13
|
199 |
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
|
200 |
|
sawine@13
|
201 |
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
|
202 |
|
sawine@18
|
203 |
\subsection{Semantics}
|
sawine@19
|
204 |
\begin{def:frames}
|
sawine@22
|
205 |
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
|
206 |
\end{def:frames}
|
sawine@19
|
207 |
|
sawine@18
|
208 |
\begin{def:models}
|
sawine@22
|
209 |
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
|
210 |
%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
|
211 |
\end{def:models}
|
sawine@13
|
212 |
|
sawine@18
|
213 |
\begin{def:satisfiability}
|
sawine@19
|
214 |
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
|
215 |
\begin{itemize}
|
sawine@22
|
216 |
\item $\M,i \models p$ for $p \in \Prop \iff p \in V(i)$
|
sawine@22
|
217 |
\item $\M,i \models \neg \varphi \iff$ not $\M,i \models \varphi$
|
sawine@22
|
218 |
\item $\M,i \models \varphi \lor \psi \iff \M,i \models \varphi$ or $\M,i \models \psi$
|
sawine@22
|
219 |
\item $\M,i \models X \varphi \iff \M,i+1 \models \varphi$
|
sawine@22
|
220 |
\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
|
221 |
\end{itemize}
|
sawine@22
|
222 |
|
sawine@18
|
223 |
\end{def:satisfiability}
|
sawine@18
|
224 |
|
sawine@14
|
225 |
\begin{def:vocabulary}
|
sawine@22
|
226 |
Let $\varphi$ be an LTL-formula over atomic propositions $\Prop$, we define the \emph{vocabulary} $Voc(\varphi)$ of $\varphi$ inductively:
|
sawine@15
|
227 |
\begin{multicols}{2}
|
sawine@14
|
228 |
\begin{itemize}
|
sawine@19
|
229 |
\item $Voc(p) = \{p\}$ for $p \in \Prop$
|
sawine@14
|
230 |
\item $Voc(\neg \varphi) = Voc(\varphi)$
|
sawine@14
|
231 |
\item $Voc(\varphi \lor \psi) = Voc(\varphi) \cup Voc(\psi)$
|
sawine@14
|
232 |
\item $Voc(X \varphi) = Voc(\varphi)$
|
sawine@14
|
233 |
\item $Voc(\varphi U \psi) = Voc(\varphi) \cup Voc(\psi)$
|
sawine@14
|
234 |
\end{itemize}
|
sawine@15
|
235 |
\end{multicols}
|
sawine@17
|
236 |
%
|
sawine@22
|
237 |
\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
|
238 |
\[\forall{i \in \N}: V_{Voc(\varphi)}(i) = V(i) \cap Voc(\varphi)\]
|
sawine@21
|
239 |
Henceforth, we will abbreviate $\M_{Voc(\varphi)}$ and $V_{Voc(\varphi)}$ with $\M_\varphi$ and $V_\varphi$ accordingly.
|
sawine@22
|
240 |
%\noindent Let $\M$ be a model and $\varphi$ an LTL-formula, we define model $\M_{Voc(\varphi)}$:
|
sawine@21
|
241 |
%\[\forall{i \in \N}: \M_{Voc(\varphi)} = \M(i) \cap Voc(\varphi)\]
|
sawine@17
|
242 |
\end{def:vocabulary}
|
sawine@17
|
243 |
%
|
sawine@17
|
244 |
\begin{prop:vocabulary sat}
|
sawine@22
|
245 |
Let $\M$ be a model and $\varphi$ an LTL-formula, then following holds:
|
sawine@21
|
246 |
\[\forall{i \in \N}: \M,i \models \varphi \iff \M_\varphi,i \models \varphi\]
|
sawine@17
|
247 |
\end{prop:vocabulary sat}
|
sawine@17
|
248 |
%
|
sawine@19
|
249 |
\subsection{Derived connectives}
|
sawine@17
|
250 |
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
|
251 |
|
sawine@19
|
252 |
Let $\varphi$ and $\psi$ be $L_{LTL}(\Prop)$-formulae:
|
sawine@15
|
253 |
\begin{multicols}{2}
|
sawine@15
|
254 |
\begin{itemize}
|
sawine@19
|
255 |
\item $\top \equiv p \lor \neg p$ for $p \in \Prop$
|
sawine@15
|
256 |
\item $\bot \equiv \neg \top$
|
sawine@15
|
257 |
\item $\varphi \land \psi \equiv \neg (\neg \varphi \lor \neg \psi)$
|
sawine@15
|
258 |
\item $\varphi \rightarrow \psi \equiv \neg \varphi \lor \psi$
|
sawine@15
|
259 |
\item $\varphi \leftrightarrow \psi \equiv (\varphi \rightarrow \psi) \land (\psi \rightarrow \varphi)$
|
sawine@15
|
260 |
\item $\Diamond \varphi \equiv \top U \varphi$
|
sawine@15
|
261 |
\item $\Box \varphi \equiv \neg \Diamond \neg \varphi$
|
sawine@15
|
262 |
\end{itemize}
|
sawine@15
|
263 |
\end{multicols}
|
sawine@16
|
264 |
From the derivations for operators $\Diamond$, \emph{read diamond}, and $\Box$, \emph{read box}, it follows:
|
sawine@17
|
265 |
\begin{multicols}{2}
|
sawine@16
|
266 |
\begin{itemize}
|
sawine@17
|
267 |
\item $\M,i \models \Diamond \varphi$ iff $\exists{k \geq i}: \M,k \models \varphi$
|
sawine@17
|
268 |
\item $\M,i \models \Box \varphi$ iff $\forall{k \geq i}: \M,k \models \varphi$
|
sawine@16
|
269 |
\end{itemize}
|
sawine@17
|
270 |
\end{multicols}
|
sawine@19
|
271 |
|
sawine@19
|
272 |
With the additional derived connectives we get the following $L_{LTL}(\Prop)$-formulae productions:
|
sawine@19
|
273 |
\[\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
|
274 |
|
sawine@21
|
275 |
\section{Automata construction}
|
sawine@22
|
276 |
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 \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), ...$.
|
sawine@22
|
277 |
\[Mod(\varphi) = \{rep(\M_\varphi) \mid \M_\varphi = (\F, V_\varphi) \land \M_\varphi,0 \models \varphi\}\]
|
sawine@21
|
278 |
$Mod(\varphi)$ is the set of all infinite words, which represent models for $\varphi$.
|
sawine@21
|
279 |
|
sawine@22
|
280 |
\begin{def:fs closure}
|
sawine@22
|
281 |
Let $\varphi$ be an LTL-formula, then the \emph{Fischer-Ladner closure} $FL(\varphi)$ of $\varphi$ is the smallest set of formulae such that following holds:
|
sawine@22
|
282 |
%\begin{multicols}{2}
|
sawine@22
|
283 |
\begin{itemize}
|
sawine@22
|
284 |
\item $\varphi \in FL(\varphi)$
|
sawine@22
|
285 |
\item $\neg \psi \in FL(\varphi) \implies \psi \in FL(\varphi)$
|
sawine@22
|
286 |
\item $\psi \in FL(\varphi) \implies \neg \psi \in FL(\varphi)$
|
sawine@22
|
287 |
\item $\psi \lor \chi \in FL(\varphi) \implies \psi, \chi \in FL(\varphi)$
|
sawine@22
|
288 |
\item $X \psi \in FL(\varphi) \implies \psi \in FL(\varphi)$
|
sawine@22
|
289 |
\item $\psi U \chi \in FL(\varphi) \implies \psi, \chi, X(\psi U \chi) \in FL(\varphi)$
|
sawine@22
|
290 |
\end{itemize}
|
sawine@22
|
291 |
%\end{multicols}
|
sawine@22
|
292 |
\end{def:fs closure}
|
sawine@22
|
293 |
|
sawine@22
|
294 |
\noindent Let $FL(\varphi)$ be the closure of formula $\varphi$, we define a subset with the \emph{until}-formulae of the closure $\mathbb{U}_\varphi \subseteq FL(\varphi)$ where:
|
sawine@22
|
295 |
\[\mathbb{U}_\varphi = \{\psi U \chi \in FL(\varphi)\} \text{ and } \mathbb{U}_{\varphi_i} \text{ denotes the $i^{th}$ element of } \mathbb{U_\varphi}\]
|
sawine@22
|
296 |
|
sawine@22
|
297 |
\begin{def:atoms}
|
sawine@23
|
298 |
Let $\varphi$ be a formula and $FL(\varphi)$ its closure. $A \subseteq FL(\varphi)$ is an \emph{atom} if following holds:
|
sawine@22
|
299 |
\begin{itemize}
|
sawine@23
|
300 |
\item $\forall{\psi \in FL(\varphi)}: \psi \in A \iff \neg \psi \notin A$
|
sawine@23
|
301 |
\item $\forall{\psi \lor \chi \in FL(\varphi)}: \psi \lor \chi \in A \iff \psi \in A$ or $\chi \in A$
|
sawine@23
|
302 |
\item $\forall{\psi U \chi \in FL(\varphi)}: \psi U \chi \in A \iff \chi \in A$ or $\psi, X(\psi U \chi) \in A$
|
sawine@22
|
303 |
\end{itemize}
|
sawine@23
|
304 |
We define the set of all atoms of formula $\varphi$ with $\mathbb{AT}_\varphi = \{A \subseteq FL({\varphi}) \mid A \text{ is an atom}\}$.
|
sawine@22
|
305 |
\end{def:atoms}
|
sawine@22
|
306 |
|
sawine@22
|
307 |
\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
|
308 |
\begin{itemize}
|
sawine@22
|
309 |
\item $\Sigma = 2^{Voc(\varphi)}$
|
sawine@22
|
310 |
\item $S = \mathbb{AT_\varphi}$
|
sawine@23
|
311 |
\item $S_0 = \{A \in \mathbb{AT_\varphi} \mid \varphi \in A\}$
|
sawine@22
|
312 |
%\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@23
|
313 |
\item $\Delta = \{(A, P, \mathbb{B}) \mid A, \mathbb{B} \in \mathbb{AT_\varphi}, P = A \cap Voc(\varphi), X \psi \in A \iff \psi \in \mathbb{B}\}$
|
sawine@23
|
314 |
\item $\forall{i \in \N, i < k = |\mathbb{U}_{FL(\varphi)}|}: F_i = \{A \in \mathbb{AT}_\varphi \mid \psi U \chi \notin A$ or $\chi \in A\}$
|
sawine@23
|
315 |
\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
|
316 |
%Let $A, B \in \mathbb{AT}$ and $P \subseteq Voc(\varphi)$. Then $(A, P, B) \in \Delta$ iff the following holds:
|
sawine@22
|
317 |
%$P = A \cap Voc(\varphi)$ and For all $X \psi \in CL(\varphi): X \psi \in A$ iff $\psi \in B$.
|
sawine@22
|
318 |
\end{itemize}
|
sawine@22
|
319 |
|
sawine@22
|
320 |
\begin{thm:model language}
|
sawine@22
|
321 |
Let $\M_\varphi = (\F, V_\varphi)$ be a model and $rep(\M_\varphi)$ its infinite representation word, then following holds:
|
sawine@23
|
322 |
\[rep(\M_\varphi) \in L(\A_\varphi) \iff \M_\varphi,0 \models \varphi\]
|
sawine@22
|
323 |
\end{thm:model language}
|
sawine@22
|
324 |
\noindent
|
sawine@22
|
325 |
\begin{proof}
|
sawine@22
|
326 |
For the eloberate proof, consult \cite{ref:ltl&büchi}.
|
sawine@22
|
327 |
\end{proof}
|
sawine@22
|
328 |
|
sawine@21
|
329 |
|
sawine@8
|
330 |
\section{Model checking}
|
sawine@15
|
331 |
|
sawine@19
|
332 |
|
sawine@19
|
333 |
\section{On-the-fly methods}
|
sawine@19
|
334 |
|
sawine@0
|
335 |
\begin{thebibliography}{99}
|
sawine@5
|
336 |
\bibitem{ref:ltl&büchi}
|
sawine@6
|
337 |
\uppercase{M{\footnotesize adhavan} M{\footnotesize ukund}.}
|
sawine@5
|
338 |
{\em Linear-Time Temporal Logic and B\"uchi Automata}.
|
sawine@2
|
339 |
Winter School on Logic and Computer Science, Indian Statistical Institute, Calcutta, 1997.
|
sawine@0
|
340 |
|
sawine@2
|
341 |
\bibitem{ref:handbook}
|
sawine@6
|
342 |
\uppercase{P{\footnotesize atrick} B{\footnotesize lackburn},
|
sawine@6
|
343 |
F{\footnotesize rank} W{\footnotesize olter and} J{\footnotesize ohan van} B{\footnotesize enthem}.}
|
sawine@2
|
344 |
{\em Handbook of Modal Logic (Studies in Logic and Practical Reasoning)}.
|
sawine@3
|
345 |
3rd Edition, Elsevier, Amsterdam, 2007.
|
sawine@7
|
346 |
|
sawine@19
|
347 |
\bibitem{ref:alternating verification}
|
sawine@19
|
348 |
\uppercase{M{\footnotesize oshe} Y. V{\footnotesize ardi}.}
|
sawine@19
|
349 |
{\em Alternating Automata and Program Verification}.
|
sawine@19
|
350 |
Computer Science Today, Volume 1000 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1995.
|
sawine@19
|
351 |
|
sawine@7
|
352 |
\bibitem{ref:infpaths}
|
sawine@7
|
353 |
\uppercase{P{\footnotesize ierre} W{\footnotesize olper},
|
sawine@7
|
354 |
M{\footnotesize oshe} Y. V{\footnotesize ardi and}
|
sawine@7
|
355 |
A. P{\footnotesize rasad} S{\footnotesize istla}.}
|
sawine@7
|
356 |
{\em Reasoning about Infinite Computation Paths}.
|
sawine@7
|
357 |
In Proceedings of the 24th IEEE FOCS, 1983.
|
sawine@7
|
358 |
|
sawine@0
|
359 |
\end{thebibliography}
|
sawine@0
|
360 |
\end{document}
|