Please use this identifier to cite or link to this item: http://doi.org/10.25358/openscience-4424
Authors: Beber, Björn
Title: Improving interpolants of non-convex polyhedra with linear arithmetic and probably approximatley correct learning for bounded linear arrangements
Online publication date: 22-May-2018
Year of first publication: 2018
Language: english
Abstract: This thesis is split into two parts. In the first part on the top level is a modelchecking algorithm, which verifies safety properties of a linearhybrid automaton. During computation it has to handle intermediate state sets, which are described as non-convex polyhedra, i.e. subsets of R^n×B^m with linear hyperplanes as boundaries. The computation of this algorithm had problems handling the huge amount of linear constraints in the description of those state sets. Therefore we compute a Craig interpolant of the state set Φ and the complement of an epsilon-bloated state set Φ′ = (Φ ∪ Φ_ε)^C , with a preferably lower amount of linear constraints. We propose an algorithm that reduces the number of constraints of a given interpolant for the pair (Φ,Φ′) of state sets. The approach is to select two linear constraints of the current interpolant and, if successful, substitute it by only one new linear constraint. Additionally, we propose two applications of this algorithm in similar context. With the first application we construct lower bounds for the problem above, in the specific case that Φ and Φ′ share the same boundary. As a second application we propose an algorithm to reduce the number of bits used in the description of a state set, while limiting the overapproximation by taking a superset of the given state set into account. Our results show that the quality of our main algorithm is superior to all related algorithms. In addition it is even faster than all related algorithms, when we do not count the algorithm that only removes redundant linear constraints. In the second part we switch to the context of theoretical machine learning. More specifically we propose an algorithm that is a Probably Approximately Correct learning algorithm for the concept class of bounded linear arrangements in fixed dimension. Furthermore we introduce an Integer Linear Program (ILP) that models this problem, which then is solved by a Column Generation approach to handle the large amount of variables used in the ILP . Finally we speed up the algorithm by a randomized approach. Instead of taking all samples into account at once, we build up a subset of samples that consists of significant samples. Additionally to the theoretical results, our evaluation confirms that our final approach can handle more reasonable datasets.
Diese Arbeit ist in zwei Abschnitte unterteilt. Im ersten Teil ist unser Problem angesiedelt als Anwendung für einen Model-CheckingAlgorithmus, der sicherheitskritische Eigenschaften eines linearen hybriden Automaten verifiziert. Für die Berechnung werden Zustandsmengen als nicht konvexe Polyeder beschrieben, d. h. Mengen aus R^n×B^m dessen Grenzen durch lineare Hyperebenen beschrieben werden. Die Berechnungszeit des Algorithmus scheitert an zu großen Mengen von linearen Hyperebenen in der Beschreibung der Zustandsmengen. Wir suchen eine Craig Interpolante für eine Zustandsmenge Φ und dem Komplement der um Epsilon erweiterten Zustandsmenge Φ′ = (Φ ∪ Φ_ε)^C mit einer möglichst geringen Anzahl an linearen Ungleichungen. Wir stellen einen Ansatz vor, der die Anzahl an linearen Ungleichungen einer gegebenen Interpolante für ein Paar von Zustandsmengen (Φ,Φ′) reduziert. Unser Ansatz wählt zwei lineare Ungleichungen aus der momentanen Interpolante aus und versucht diese durch eine neu berechnete Ungleichung zu ersetzen. Zusätzlich stellen wir zwei Anwendungen unseres Algorithmus in dem Kontext des ModelChecking-Algorithmus vor. Als erste Anwendung berechnen wir untere Schranken für unser Problem in dem Fall, dass sich beide Zustandsmengen Φ und Φ′ eine gemeinsame Grenze teilen. Die zweite Anwendung reduziert die Anzahl der verwendeten Bits in der Beschreibung einer Zustandsmenge unter Berücksichtigung einer Obermenge. Durch unsere Analyse zeigen wir, dass die Qualität unseres Hauptalgorithmus besser ist, als die verwandter Methoden. Zusätzlich ist unsere Methode schneller als alle verwandten Methoden, wenn man die Methode vernachlässigt, die nur Redundanzen beseitigt. Im zweiten Teil beschäftigen wir uns mit dem Thema des theoretischen maschinellen Lernens, insbesondere mit dem Wahrscheinlich Annähernd Richtigen Lernen (PAC). Wir stellen einen PAC-Lerner für beschränkte lineare Anordnungen in fixierter Dimension vor. Zudem modellieren wir ein Ganzzahliges Lineares Programm und lösen dieses mit Spaltengenerierung, um mit der großen Menge an Variablen umgehen zu können. Als letzte ausschlaggebende Verbesserung stellen wir einen randomisierten Ansatz vor. Statt alle Proben gleichzeitig zu betrachten, baut der randomisierte Ansatz eine Teilmenge von charakteristischen Proben auf. Zusätzlich zu den theoretischen Resultaten zeigt die Analyse, dass unser endgültiger Algorithmus deutlich komplexere Benchmarks berechnen kann, als der Basis-Algorithmus.
DDC: 004 Informatik
004 Data processing
Institution: Johannes Gutenberg-Universität Mainz
Department: FB 08 Physik, Mathematik u. Informatik
Place: Mainz
ROR: https://ror.org/023b0x485
DOI: http://doi.org/10.25358/openscience-4424
URN: urn:nbn:de:hebis:77-diss-1000020064
Version: Original work
Publication type: Dissertation
License: In Copyright
Information on rights of use: https://rightsstatements.org/vocab/InC/1.0/
Extent: xi, 135 Seiten
Appears in collections:JGU-Publikationen

Files in This Item:
  File Description SizeFormat
Thumbnail
100002006.pdf661.31 kBAdobe PDFView/Open