\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

\title{A Verified Algorithm for Geometric Zonotope/Hyperplane Intersection}
\author{Fabian Immler}

\begin{document}

\maketitle

\begin{abstract}

To perform rigorous numerical computations, one can use a generalization of
interval arithmetic, namely affine arithmetic (AA), which works with zonotopes
instead of intervals. Zonotopes are also widely used for reachability analysis
of continuous or hybrid systems, where an important operation is the geometric
intersection of zonotopes with hyperplanes.

We have implemented a functional algorithm to compute the zonotope/hyperplane
intersection and verified it in Isabelle/HOL. The algorithm is similar to convex
hull computations, our verification is therefore inspired by Knuth's axioms for
an orientation predicate of points in the plane, which have been successfully
used to verify convex hull algorithms. The interesting fact is that we combine a
mixture of different fields: a discrete geometrical algorithm to perform
operations on the continuous sets represented by zonotopes.

\end{abstract}

\section{Relations to the paper}

Here we relate the contents of the submission~\cite{Immler} for CPP~2015 with the sources of our
developments. In the following list we show which notions and theorems in the paper correspond to
which parts of the source code.

\begin{enumerate}
\item Introduction
\item Background from Analytic Geometry
\item Affine Arithmetic: definition is type of \textit{pdevs} in section~\ref{sec:aforms},
  range and joint range is \textit{Affine} and \textit{Joints}.
  Theorem~3.1 on addition of affine forms is a special case of lemma \textit{pdevs-val-add-pdevs}
\item Intersection: the corresponding formalization is in section~\ref{sec:intersection}
  \begin{enumerate}
  \item Reduction to a Two-Dimensional Problem: theorem~4.1 is lemma \textit{inter-overappr},
    \textit{bound-intersect-2D} is formalized under the same name, and it is based on the
      intersection of edges with vertical lines as implemented in \textit{intersect-segment-xline}
  \item Computation of Two-Dimensional Hulls: \textit{hull-of-zonotope}
    is formalized as \textit{segments-of-aform}
  \end{enumerate}
\item Geometry:
  \begin{enumerate}
  \item CCW systems: the abstract theory is formalized in section~\ref{sec:counterclockwise}.
  \item Total Order from CCW: see section~\ref{sec:ccworder}
  \item Instantiation for Points in the Plane: in section~\ref{sec:counterclockwise2d}
  \item CCW on a Vector Space: theorems 5.7 and 5.8 can are formalized as \textit{det3-pos-translate-plus}
    and \textit{det3-zero-scaleR2}
  \end{enumerate}
\item Verification of Two-Dimensional Hulls:
  \begin{enumerate}
  \item Appending Sorted Vectors: lemma~6.1 is formalized as lemma \textit{polychain-of-ccw}
  \item The Interior of the Zonotope: lemma~6.2 is formalized as lemma \textit{half-segments-of-aform-strict},
    but \textit{half-segments-of-aform} already includes the preprocessing.
  \item Reflected Corners: lemma~6.3 is formalized as lemma \textit{segments-of-aform-strict}
  \item ``Postprocessing'': Continuously Relaxing CCW: theorem~6.4 is lemma \textit{ccw-coll-segments-of-aform}
  \item Preprocessing for Generators: preprocessing is done in the definition of
    \textit{half-segments-of-aform}, by using \textit{dnu}, which is based on \textit{upward-pdevs} to
    sort the generators upwards and \textit{independent-pdevs} to filter collinear generators.
  \end{enumerate}
\item The Final Intersection Algorithm: correctness of intersection based on Basis-parallel
  directions is given in lemma \textit{inter-inter-aform-plane-ortho}
\item Experiments: are conducted in section~\ref{sec:examples}
\item Conclusion
\item A Consistent CCW Predicate for Degenerate Cases: is given by
  \textit{interpretation ccw-system ccw}
\end{enumerate}

\tableofcontents

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
