Improving interpolants of non-convex polyhedra with linear arithmetic and probably approximatley correct learning for bounded linear arrangements
Date issued
Authors
Editors
Journal Title
Journal ISSN
Volume Title
Publisher
License
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.