-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathmain.tex
315 lines (248 loc) · 15.5 KB
/
main.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
% easychair.tex,v 3.4 2016/10/19
\documentclass[EPiC]{easychair}
\usepackage{doc}
\usepackage{tikz}
\usepackage{subfigure}
\usepackage{tabularx}
\usepackage{booktabs}
\usepackage{framed}
\usepackage{amsmath,amssymb,amsfonts}
\usepackage{hyperref}
\usepackage[defaultlines=4,all]{nowidow}
\usepackage{enumitem} % GF 2017-03-28
\usepackage{tablefootnote}
\usepackage{cleveref}
\usepackage{xcolor}
\usepackage{floatrow}
\usepackage{tikz}
\usepackage{pbox}
\usepackage{pgfplots}
%% - Utils
\newlength{\plotwidth}
\setlength{\plotwidth}{0.45\columnwidth}
\newlength{\plotwidthShort}
\setlength{\plotwidthShort}{0.4\columnwidth}
\input{commands}
\newcommand{\todo}[1]{
\begin{framed}
\noindent{\bf TODO: }
#1
\end{framed}
}
\newcommand{\remark}[1]{
\begin{framed}
\noindent{\bf Remark: }
#1
\end{framed}
}
%\makeindex
%% Front Matter
%%
% Regular title as in the article class.
%
\title{ARCH-COMP18 Category Report:\\ Stochastic Modelling}
% Authors are joined by \and. Their affiliations are given by \inst, which indexes
% into the list defined using \institute
% Author order: first author is group leader, other authors are added alphabetically
\author{Alessandro Abate \inst{1}
\and Henk Blom \inst{2}
\and Nathalie Cauchi \inst{1}
\and Sofie Haesaert \inst{3}
\and Arnd Hartmanns \inst{4}
\and Meeko Oisho \inst{5}
\and Vignesh Sivaramakrishnan \inst{5}
\and Sadegh Soudjani \inst{6}
\and Cristian-Ioan Vasile \inst{7}
\and Abraham Vinod \inst{5}
}
% Institutes for affiliations are also joined by \and,
\institute{University of Oxford, Department of Computer Science, Oxford, UK
\email{[email protected]}
\and
\and
\and
\and
\and
School of Computing, Newcastle University, UK, \email{[email protected]}
\and
}
% \authorrunning{} has to be set for the shorter version of the authors' names;
% otherwise a warning will be rendered in the running heads. When processed by
% EasyChair, this command is mandatory: a document without \authorrunning
% will be rejected by EasyChair
\authorrunning{}
% \titlerunning{} has to be set to either the main title or its shorter
% version for the running heads. When processed by
% EasyChair, this command is mandatory: a document without \titlerunning
% will be rejected by EasyChair
\titlerunning{ARCH-COMP18 Stochastic models}
\begin{document}
\maketitle
\todo{Add all affiliations}
\begin{abstract}
This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. The friendly competition took place as part of the workshop \underline{A}pplied Ve\underline{r}ification for \underline{C}ontinuous and \underline{H}ybrid Systems (ARCH) in 2018.
\end{abstract}
%------------------------------------------------------------------------------
\section{Introduction}
\label{sect:introduction}
\begin{framed}
\paragraph{Disclaimer} The presented report of the ARCH friendly competition for \textit{stochastic modelling group} which aims at providing a landscape ....
\end{framed}
This report summarizes results obtained in the 2018 friendly competition of the ARCH workshop\footnote{Workshop on \underline{A}pplied Ve\underline{r}ification for \underline{C}ontinuous and \underline{H}ybrid Systems (ARCH), \href{http://cps-vo.org/group/ARCH}{cps-vo.org/group/ARCH}} for\\
The goal of the friendly competition is not to rank the results, but rather to present the landscape of existing solutions in a breadth that is not possible with scientific publications in classical venues. Such publications would typically require the presentation of novel techniques, while this report showcases the current state-of-the-art tools. For all results reported by each participant, we have run an independent repeatability evaluation.
\hrmkNMC{To complete}
%------------------------------------------------------------------------------
\section{Benchmarks}
\label{sec:benchmarks}
We introduce a new category for the 2018 edition and with it a new set of benchmarks: an anesthesia delivery system, building automation system, a heated tank, a lawn mover and a mars rover. Each benchmark is characterised with special features which we delineate first. Next, we discuss each benchmark, the different problems to be solved together with specifications of interest, and different paths to successfully verifying a benchmark. Afterwards, the verification of each benchmark is presented in detail. \\
\paragraph{Special features} We briefly list the key features of each benchmark:
\begin{itemize}
\item \textit{Anesthesia delivery system benchmark}:
\item \textit{Building automation benchmark}: this benchmark is based on a library of models describing different components within a heating system. We focus on two instances of possible benchmarks which describe discrete-time linear systems with varying numbers of continuous state variables. The benchmark focuses on safety properties.
\item \textit{Heated tank benchmark}:
\item \textit{Lawn mower benchmark}: this benchmark focuses on controller synthesis and verification for a driverless industrial size lawn mower. While a number of diverse schemes can be used for synthesizing a controller, we use one that has a simple switching mechanism for guiding the mower between way-points in the field. We describe continuous-time dynamics of the mower together with the controller. The closed-loop model fits into the framework of continuous-time hybrid systems, which has 6 continuous states (with possibility of extending to 8), two discrete modes, and nonlinear drift functions in each mode.
Although statistical techniques such as multilevel Monte Carlo method \cite{MLMC_SRN_17} can be used to verify properties of the \emph{continuous-time} dynamics,
We transform the model into \emph{discrete-time polynomial} dynamics and use barrier certificates \textcolor{blue}{\cite{}} for the verification task.
\item \textit{Mars rover benchmark}:
\end{itemize}
\todo{Include brief description or special features of the benchmark}
%%% Benchmark descriptions together with results
\input{Anesthesia.tex}
\newpage
\input{BAS.tex}
\newpage
\input{HeatedTank.tex}
\newpage
\input{LawnMower.tex}
\newpage
\input{MarsRover.tex}
\todo{Inclusion of full benchmark descriptions}
%------------------------------------------------------------------------------
\section{Participating Tools \& Frameworks}
\label{sect:tools}
The tools and frameworks used in the category \textit{Stochastic Modelling} are introduced subsequently in alphabetical order.
\paragraph{Barrier Certificates}
The paper \cite{} provides a systematic approach of using barrier certificates for algorithmic verification of stochastic systems against a wide class of temporal properties. It provides a method for computing lower bounds on the probability that a discrete-time stochastic system satisfies given \emph{safe LTL specification} over a \emph{finite} time horizon. This is achieved by first decomposing specification into a sequence of simpler verification tasks based on the structure of the automaton associated with the negation of the specification. Then it uses barrier certificates for computing probability bounds for simpler verification tasks, which are further combined to get a lower bound on the probability of satisfying the original specification. Computation of barrier certificates can be performed for polynomial dynamics using sum-of-squares optimizations.
\paragraph{FAUST$^2$}
The tool \textit{Formal Abstractions of Uncountable-STate STochastic
processes} (FAUST$^2$) ~\cite{soudjani2015faust} generates formal abstractions of discrete-time Markov processes (dtMP) defined over continuous state spaces. The dtMP model is abstracted into a finite-state Markov chain or a Markov decision process. The abstract model is formally put in relationship with the concrete dtMP via a user-defined maximum threshold on the approximation error introduced by the abstraction procedure. FAUST$^2$ allows exporting the abstract model to well-known probabilistic model checkers,such as PRISM or MRMC. Alternatively, it can handle internally the computation of PCTL properties (e.g. safety or reach-avoid) over the abstract model, and refine the outcomes over the concrete dtMP via a quantified error that depends on the abstraction procedure and the given formula. The toolbox is available at \url{https://sourceforge.net/projects/faust2/}\\
\paragraph{Modest}
\paragraph{SReach Tools}
\todo{ Fill the appropriate description + title of tool or framework employed}
%------------------------------------------------------------------------------
\section{Results}
\label{sect:results}
We present the results obtained for each case studies using the tools highlighted in Sec.\ref{sect:tools}.
%%%%% Results for Anesthesia model
\subsection{Anesthesia benchmark}
\newpage
\subsection{Building Automation System benchmark}
\subsubsection{CS1BAS: Results}
The results obtained using the individual tools are presented hereunder.
\begin{figure}[htb]
\centering
\resizebox{0.6\columnwidth}{!}{\input{figures/PRA.tikz}
\caption{FAUST$^2$: Partition of the safe set for model $M_s$,
along with optimal safety probability for each partition set}
\label{fig:bas:faust}}
\end{figure}
\todo{add results of other tools and include computational times, description}
\subsubsection{CS2BAS: Results}
For $\mathbf{M}_c$ and the given specification aim at synthesising a policy maximising the safety probability $p$. This synthesis goal can be computationally hard due to the number of continuous variables making up $\mathbf{M}_c$.
\todo{Say how each tool tackles this}
\textcolor{blue}{Barrier certificate method is not applicable to this benchmark since it is computationally restricted to \emph{verification} of \emph{time-invariant} systems.
We are working on extensions to synthesis, but the results are not ready yet.
}
\paragraph{Results using FAUST$^2$}
In order to make use of the FAUST$^2$, we perform policy synthesis via abstractions and $(\varepsilon,\delta)$ simulation relations~\cite{peva}. The $(\varepsilon,\delta)$ pair providing the optimal trade off is obtained using an abstract model with 1 continuous variable and corresponds to ($0.2854,$ $ 10^{-2}$).
Next, we use FAUST$^2$ to perform a grid-based computation of the safety probability on the abstract model and obtain a model of size 14893 with an overall accuracy of $0.005$.
Over this approximation we synthesise the optimal policy for the abstract model which results in a safety probability of $p'= 0.9257$. We refine the obtained policy~\cite{peva} such that it can be applied to the original model~\eqref{eqn:Mc}. The overall process results in $\Phi$ being satisfied with a safety probability of $p = p'-\eta - N\delta = 0.7657$, where $\eta$ is the abstraction error introduced by FAUST$^2$.
\todo{add results of other tools and include computational times, description}
\newpage
\subsection{Heated Tank benchmark}
\textcolor{blue}{Barrier certificate method is not applicable to this benchmark since it is computationally restricted to discrete-time polynomial dynamics.}
\newpage
\subsection{Lawn Mower benchmark}
\subsubsection{Verification using Barrier Certificate}
We use Barrier Certificates for computing bounds on reachability probability. More specifically, the approach has been recently developed for computing lower bound on probability of satisfying a \emph{safe LTL specification}. Thus, it can be used for finding upper bounds on reachability properties.
Computationally, the approach is developed for discrete-time stochastic systems with polynomial dynamics and uses sum-of-squares optimization techniques for finding such bounds.
\noindent
\textbf{Transformation to discrete-time polynomial dynamics.}
The dynamics of the lawn mower is not polynomial. We employ a nonlinear transformation of the states to get polynomial vector fields with polynomial constraints.
%
%To make dynamics compatible for computation of barrier certificates using SOS solvers
We do coordinate transform as
$$[y_1,y_2 y_3,y_4,y_5,y_6]=[x_2,\tan\Big( \frac{2(x_2-bx_1)}{(V_r+V_l)}\Big ),x_3,x_4,x_5,x_6].$$
%
%The controller \eqref{eq:controller} in the new coordinates can be simplified to
%We consider that the mower is driven by switched controller given by
%$$V_l=V_b+V_d \text{ sgn}(\sin(y_5)(x_d-y_3)-\cos(y_5)(y_d-y_4)),$$ $$V_r=V_b-V_d \text{ sgn}(\sin(y_5)(x_d-y_3)-\cos(y_5)(y_d-y_4)).$$
%
The discrete-time closed-loop dynamics are given as
\begin{align*}
y_1(k+1) &=y_1(k)+T_s\left(\frac{1}{I_{zz}}(A_{fy} z_4(k) a+2C_{\gamma} y_2(k)*b)\right),\\
y_2(k+1) &=y_2(k)+T_s\left(\frac{2(1+y_2(k)^2)}{V_r(k)+V_l(k)}\Big(\frac{1}{M}(A_{fy}z_4(k)-2C_{\gamma}y_2(k))\right.\\
&\hspace{3cm}\left.-\frac{V_r(k)+V_l(k)}{2}y_1(k)-\frac{b}{I_{zz}}(A_{fy} z_4(k) a+2C_{\gamma} y_2(k)b)\Big)\right),\\
y_3(k+1) &=y_3(k)+T_s\left(\frac{V_r(k)+V_l(k)}{2}z_2(k)\right),\\
y_4(k+1) &=y_4(k)+T_s\left(\frac{V_r(k)+V_l(k)}{2}z_1(k)\right),\\
y_5(k+1) &=y_5(k)+T_s\left(\frac{V_r(k)-V_l(k)}{2D}+y_1(k)\right)+w_1(k),\\
y_6(k+1) &=y_6(k)+T_s\left(-\frac{V_r(k)+V_l(k)}{2d}z_4(k)-\frac{(V_r(k)-V_l(k))(d+\sqrt{D^2+(a+b)^2} z_3(k))}{2Dd}\right)+w_2(k),
\end{align*}
where $z_1=\sin(y_5)$, $z_2=\cos(y_5)$, $z_3=\sin(y_6)$, $z_4=\cos(y_6)$, and $T_s$ is a sampling time.
The controller \eqref{eq:controller} in the new coordinates can be simplified to
%Based on the controller mentioned above, we get
two modes of operation depending on location in state space as
%and are obtained by using
\begin{equation*}
\begin{cases}
V_l=V_b-V_d, V_r=V_b+V_d , & \text{if }z_1(x_d-y_3)-z_2(y_d-y_4)<0\\
V_l=V_b+V_d, V_r=V_b-V_d , & \text{if }z_1(x_d-y_3)-z_2(y_d-y_4)>0.
\end{cases}
\end{equation*}
The lower bound $\alpha = 0.8852$ is obtained using YALMIP and SeDuMi for initial states starting from $X_0$ with the help of barrier certificate of order 2.
\newpage
\subsection{Mars Rover benchmark}
%------------------------------------------------------------------------------
\section{Conclusion and Outlook}
\label{sect:conclusion}
This report presents the results on a first friendly competition for the formal verification of stochastic models as part of the ARCH'18 workshop. The reports of other categories can be found in the proceedings and on the ARCH website: \href{http://cps-vo.org/group/ARCH}{cps-vo.org/group/ARCH}.
\todo{
\begin{itemize}
\item General observations and difficulties encountered
\item Future goals and desired outcomes
\end{itemize}
}
%------------------------------------------------------------------------------
\section{Acknowledgments}
\label{sec:acks}
This work is partially supported by the Alan Turing Institute, UK; Malta's ENDEAVOUR Scholarships Scheme; and the NWO SEQUOIA project.
%------------------------------------------------------------------------------
\appendix
\section{Specification of Used Machines} \label{sec:machines}
\subsection{M$_{\text{Barrier Certificates}}$} \label{sec:machine:bc}
\begin{itemize}
\item Processor:
\item Memory:
\item Average CPU Mark on \url{www.cpubenchmark.net}:
\end{itemize}
\subsection{M$_{\text{FAUST$^2$}}$} \label{sec:machine:faust2}
\begin{itemize}
\item Processor: Intel Core i7-8550U CPU @ 1.80GHz $\times$ 8
\item Memory: 8 GB
\item Average CPU Mark on \url{www.cpubenchmark.net}: 8337
\end{itemize}
\subsection{M$_{\text{Modest}}$} \label{sec:machine:Modest}
\begin{itemize}
\item Processor:
\item Memory:
\item Average CPU Mark on \url{www.cpubenchmark.net}:
\end{itemize}
\subsection{M$_{\text{SReachTools}}$} \label{sec:machine:SReachTools}
\begin{itemize}
\item Processor:
\item Average CPU Mark on \url{www.cpubenchmark.net}:
\end{itemize}
\todo{Please add own specs}
\bibliographystyle{plain}
\bibliography{bib/Cauchibib.bib}
\end{document}