Fakultät für Mathematik, Informatik und Statistik - Digitale Hochschulschriften der LMU - Teil 01/02

The ongoing automation in our modern information society leads to a tremendous rise in the amount as well as complexity of collected data. In medical imaging for example the electronic availability of extensive data collected as part of clinical trials provides a remarkable potentiality to detect new relevant features in complex diseases like brain tumors. Using data mining applications for the analysis of the data raises several problems. One problem is the localization of outstanding observations also called outliers in a data set. In this work a technique for parameter-free outlier detection, which is based on data compression and a general data model which combines the Generalized Normal Distribution (GND) with independent components, to cope with existing problems like parameter settings or implicit data distribution assumptions, is proposed. Another problem in many modern applications amongst others in medical imaging is the efficient similarity search in uncertain data. At present, an adequate therapy planning of newly detected brain tumors assumedly of glial origin needs invasive biopsy due to the fact that prognosis and treatment, both vary strongly for benign, low-grade, and high-grade tumors. To date differentiation of tumor grades is mainly based on the expertise of neuroradiologists examining contrast-enhanced Magnetic Resonance Images (MRI). To assist neuroradiologist experts during the differentiation between tumors of different malignancy we proposed a novel, efficient similarity search technique for uncertain data. The feature vector of an object is thereby not exactly known but is rather defined by a Probability Density Function (PDF) like a Gaussian Mixture Model (GMM). Previous work is limited to axis-parallel Gaussian distributions, hence, correlations between different features are not considered in these similarity searches. In this work a novel, efficient similarity search technique for general GMMs without independence assumption is presented. The actual components of a GMM are approximated in a conservative but tight way. The conservativity of the approach leads to a filter-refinement architecture, which guarantees no false dismissals and the tightness of the approximations causes good filter selectivity. An extensive experimental evaluation of the approach demonstrates a considerable speed-up of similarity queries on general GMMs. Additionally, promising results for advancing the differentiation between brain tumors of different grades could be obtained by applying the approach to four-dimensional Magnetic Resonance Images of glioma patients.

One of the main design goals of social software, such as wikis, is to

support and facilitate interaction and collaboration. This dissertation

explores challenges that arise from extending social software with

advanced facilities such as reasoning and semantic annotations and

presents tools in form of a conceptual model, structured tags, a rule

language, and a set of novel forward chaining and reason maintenance

methods for processing such rules that help to overcome the

challenges.

Wikis and semantic wikis were usually developed in an ad-hoc

manner, without much thought about the underlying concepts. A conceptual

model suitable for a semantic wiki that takes advanced features

such as annotations and reasoning into account is proposed. Moreover,

so called structured tags are proposed as a semi-formal knowledge

representation step between informal and formal annotations.

The focus of rule languages for the Semantic Web has been predominantly

on expert users and on the interplay of rule languages

and ontologies. KWRL, the KiWi Rule Language, is proposed as a

rule language for a semantic wiki that is easily understandable for

users as it is aware of the conceptual model of a wiki and as it

is inconsistency-tolerant, and that can be efficiently evaluated as it

builds upon Datalog concepts.

The requirement for fast response times of interactive software

translates in our work to bottom-up evaluation (materialization) of

rules (views) ahead of time – that is when rules or data change, not

when they are queried. Materialized views have to be updated when

data or rules change. While incremental view maintenance was intensively

studied in the past and literature on the subject is abundant,

the existing methods have surprisingly many disadvantages – they

do not provide all information desirable for explanation of derived

information, they require evaluation of possibly substantially larger

Datalog programs with negation, they recompute the whole extension

of a predicate even if only a small part of it is affected by a

change, they require adaptation for handling general rule changes.

A particular contribution of this dissertation consists in a set of

forward chaining and reason maintenance methods with a simple declarative

description that are efficient and derive and maintain information

necessary for reason maintenance and explanation. The reasoning

methods and most of the reason maintenance methods are described

in terms of a set of extended immediate consequence operators the

properties of which are proven in the classical logical programming

framework. In contrast to existing methods, the reason maintenance methods in this dissertation work by evaluating the original Datalog

program – they do not introduce negation if it is not present in the input

program – and only the affected part of a predicate’s extension is

recomputed. Moreover, our methods directly handle changes in both

data and rules; a rule change does not need to be handled as a special

case.

A framework of support graphs, a data structure inspired by justification

graphs of classical reason maintenance, is proposed. Support

graphs enable a unified description and a formal comparison of the

various reasoning and reason maintenance methods and define a notion

of a derivation such that the number of derivations of an atom is

always finite even in the recursive Datalog case.

A practical approach to implementing reasoning, reason maintenance,

and explanation in the KiWi semantic platform is also investigated. It

is shown how an implementation may benefit from using a graph

database instead of or along with a relational database.

A primary feature of a computer program is its quantitative performance characteristics: the amount of resources such as time, memory, and power the program needs to perform its task. Concrete resource bounds for specific hardware have many important applications in software development but their manual determination is tedious and error-prone.

This dissertation studies the problem of automatically determining concrete worst-case bounds on the quantitative resource consumption of functional programs.

Traditionally, automatic resource analyses are based on recurrence relations. The difficulty of both extracting and solving recurrence relations has led to the development of type-based resource analyses that are compositional, modular, and formally verifiable. However, existing automatic analyses based on amortization or sized types can only compute bounds that are linear in the sizes of the arguments of a function.

This work presents a novel type system that derives polynomial bounds from first-order functional programs. As pioneered by Hofmann and Jost for linear bounds, it relies on the potential method of amortized analysis. Types are annotated with multivariate resource polynomials, a rich class of functions that generalize non-negative linear combinations of binomial coefficients. The main theorem states that type derivations establish resource bounds that are sound with respect to the resource-consumption of programs which is formalized by a big-step operational semantics.

Simple local type rules allow for an efficient inference algorithm for the type annotations which relies on linear constraint solving only. This gives rise to an analysis system that is fully automatic if a maximal degree of the bounding polynomials is given. The analysis is generic in the resource of interest and can derive bounds on time and space usage. The bounds are naturally closed under composition and eventually summarized in closed, easily understood formulas.

The practicability of this automatic amortized analysis is verified with a publicly available implementation and a reproducible experimental evaluation. The experiments with a wide range of examples from functional programming show that the inference of the bounds only takes a couple of seconds in most cases. The derived heap-space and evaluation-step bounds are compared with the measured worst-case behavior of the programs. Most bounds are asymptotically tight, and the constant factors are close or even identical to the

optimal ones.

For the first time we are able to automatically and precisely analyze the resource consumption of involved programs such as quick sort for lists of lists, longest common subsequence via dynamic programming, and multiplication of a list of matrices with different, fitting dimensions.

The A-Translation enables us to unravel the computational information in classical proofs, by first transforming them into constructive ones, however at the cost of introducing redundancies in the extracted code. This is due to the fact that all negations inserted during translation are replaced by the computationally relevant form of the goal.

In this thesis we are concerned with eliminating such redundancies, in order to obtain better extracted programs. For this, we propose two methods: a controlled and minimal insertion of negations, such that a refinement of the A-Translation can be used and an algorithmic decoration of the proofs, in order to mark the computationally irrelevant components.

By restricting the logic to be minimal, the Double Negation Translation is no longer necessary. On this fragment of minimal logic we apply the refined A-Translation, as proposed in (Berget et al., 2002). This method identifies further selected classes of formulas for which the negations do not need to be substituted by computationally relevant formulas. However, the refinement imposes restrictions which considerably narrow the applicability domain of the A-Translation. We address this issue by proposing a controlled insertion of double negations, with the benefit that some intuitionistically

valid \Pi^0_2-formulas become provable in minimal logic and that certain formulas are transformed to match the requirements of the refined A-Translation.

We present the outcome of applying the refined A-translation to a series of examples. Their purpose is two folded. On one hand, they serve as case studies for the role played by negations, by shedding a light on the restrictions imposed by the translation method. On the other hand, the extracted programs are characterized by a specific behaviour: they adhere to the continuation passing style and the recursion is in general in tail form.

The second improvement concerns the detection of the computationally irrelevant subformulas, such that no terms are extracted from them. In order to achieve this, we assign decorations to the implication and universal quantifier. The algorithm that we propose is shown to be optimal, correct and terminating and is applied on the examples of factorial and list reversal.

The last years have seen a tremendous increase of data acquisition in different scientific fields such as molecular biology, bioinformatics or biomedicine. Therefore, novel methods are needed for automatic data processing and analysis of this large amount of data. Data mining is the process of applying methods like clustering or classification to large databases in order to uncover hidden patterns. Clustering is the task of partitioning points of a data set into distinct groups in order to minimize the intra cluster similarity and to maximize the inter cluster similarity. In contrast to unsupervised learning like clustering, the classification problem is known as supervised learning that aims at the prediction of group membership of data objects on the basis of rules learned from a training set where the group membership is known.

Specialized methods have been proposed for hierarchical and partitioning clustering. However, these methods suffer from several drawbacks. In the first part of this work, new clustering methods are proposed that cope with problems from conventional clustering algorithms. ITCH (Information-Theoretic Cluster Hierarchies) is a hierarchical clustering method that is based on a hierarchical variant of the Minimum Description Length (MDL) principle which finds hierarchies of clusters without requiring input parameters. As ITCH may converge only to a local optimum we propose GACH (Genetic Algorithm for Finding Cluster Hierarchies) that combines the benefits from genetic algorithms with information-theory. In this way the search space is explored more effectively.

Furthermore, we propose INTEGRATE a novel clustering method for data with mixed numerical and categorical attributes. Supported by the MDL principle our method integrates the information provided by heterogeneous numerical and categorical attributes and thus naturally balances the influence of both sources of information. A competitive evaluation illustrates that INTEGRATE is more effective than existing clustering methods for mixed type data. Besides clustering methods for single data objects we provide a solution for clustering different data sets that are represented by their skylines. The skyline operator is a well-established database primitive for finding database objects which minimize two or more attributes with an unknown weighting between these attributes. In this thesis, we define a similarity measure, called SkyDist, for comparing skylines of different data sets that can directly be integrated into different data mining tasks such as clustering or classification. The experiments show that SkyDist in combination with different clustering algorithms can give useful insights into many applications.

In the second part, we focus on the analysis of high resolution magnetic resonance images (MRI) that are clinically relevant and may allow for an early detection and diagnosis of several diseases. In particular, we propose a framework for the classification of Alzheimer's disease in MR images combining the data mining steps of feature selection, clustering and classification. As a result, a set of highly selective features discriminating patients with Alzheimer and healthy people has been identified. However, the analysis of the high dimensional MR images is extremely time-consuming. Therefore we developed JGrid, a scalable distributed computing solution designed to allow for a large scale analysis of MRI and thus an optimized prediction of diagnosis. In another study we apply efficient algorithms for motif discovery to task-fMRI scans in order to identify patterns in the brain that are characteristic for patients with somatoform pain disorder. We find groups of brain compartments that occur frequently within the brain networks and discriminate well among healthy and diseased people.

Parity games form an intriguing family of infinitary payoff games whose solution

is equivalent to the solution of important problems in automatic verification and

automata theory. They also form a very natural subclass of mean and discounted

payoff games, which in turn are very natural subclasses of turn-based stochastic

payoff games. From a theoretical point of view, solving these games is one of the few

problems that belong to the complexity class NP intersect coNP, and even more interestingly,

solving has been shown to belong to UP intersect coUP, and also to PLS. It is a major open

problem whether these game families can be solved in deterministic polynomial

time.

Policy iteration is one of the most important algorithmic schemes for solving

infinitary payoff games. It is parameterized by an improvement rule that determines

how to proceed in the iteration from one policy to the next. It is a major open problem

whether there is an improvement rule that results in a polynomial time algorithm for

solving one of the considered game classes.

Linear programming is one of the most important computational problems studied

by researchers in computer science, mathematics and operations research. Perhaps

more articles and books are written about linear programming than on all other

computational problems combined.

The simplex and the dual-simplex algorithms are among the most widely used

algorithms for solving linear programs in practice. Simplex algorithms for solving

linear programs are closely related to policy iteration algorithms. Like policy iteration,

the simplex algorithm is parameterized by a pivoting rule that describes how

to proceed from one basic feasible solution in the linear program to the next. It is

a major open problem whether there is a pivoting rule that results in a (strongly)

polynomial time algorithm for solving linear programs.

We contribute to both the policy iteration and the simplex algorithm by proving

exponential lower bounds for several improvement resp. pivoting rules. For every

considered improvement rule, we start by building 2-player parity games on which

the respective policy iteration algorithm performs an exponential number of iterations.

We then transform these 2-player games into 1-player Markov decision processes

ii

which correspond almost immediately to concrete linear programs on which the

respective simplex algorithm requires the same number of iterations. Additionally,

we show how to transfer the lower bound results to more expressive game classes

like payoff and turn-based stochastic games.

Particularly, we prove exponential lower bounds for the deterministic switch

all and switch best improvement rules for solving games, for which no non-trivial

lower bounds have been known since the introduction of Howard’s policy iteration

algorithm in 1960. Moreover, we prove exponential lower bounds for the two most

natural and most studied randomized pivoting rules suggested to date, namely the random

facet and random edge rules for solving games and linear programs, for which

no non-trivial lower bounds have been known for several decades. Furthermore, we

prove an exponential lower bound for the switch half randomized improvement rule

for solving games, which is considered to be the most important multi-switching

randomized rule. Finally, we prove an exponential lower bound for the most natural

and famous history-based pivoting rule due to Zadeh for solving games and linear

programs, which has been an open problem for thirty years.

Last but not least, we prove exponential lower bounds for two other classes of

algorithms that solve parity games, namely for the model checking algorithm due to

Stevens and Stirling and for the recursive algorithm by Zielonka.

In this thesis we study the geometry and topology of Riemannian 3-orbifolds which are locally volume collapsed with respect to a curvature scale. Our main result is that a sufficiently collapsed closed 3-orbifold without bad 2-suborbifolds satisfies Thurston’s Geometrization Conjecture. We also prove a version of this result with boundary. Kleiner and Lott indepedently and simultanously proved similar results ([KL11]). The main step of our proof is to construct a graph decomposition of sufficiently collapsed (closed) 3-orbifolds. We describe a coarse stratification of roughly 2-dimensional Alexandrov spaces which we then promote to a decomposition into suborbifolds for collapsed 3-orbifolds; this decomposition can then be reduced to a graph decomposition. We complete our proof by showing that graph orbifolds without bad 2-suborbifolds satisfy the Geometrization Conjecture.