This thesis proposes a diagram-based formalism for verifying temporal properties of reactive systems. Diagrams integrate deductive and algorithmic verification techniques for the verification of finite and infinite-state systems, thus combining the expressive power and flexibility of deduction with the automation provided by algorithmic methods.

Our formal framework for the specification and verification of reactive systems includes the Generalized Temporal Logic of Actions (TLA*) from Merz for both mathematical modeling reactive systems and specifying temporal properties to be verified. As verification method we adopt a class of diagrams, the so-called predicate diagrams from Cansell et al.

We show that the concept of predicate diagrams can be used to verify not only discrete systems, but also some more complex classes of reactive systems such as real-time systems and parameterized systems. We define two variants of predicate diagrams, namely timed predicate diagrams and parameterized predicate diagrams, which can be used to verify real-time and parameterized systems.

We prove the completeness of predicate diagrams and study an approach for the generation of predicate diagrams. We develop prototype tools that can be used for supporting the generation of diagrams semi-automatically.

Modern database applications are characterized by two major aspects: the use of complex data types

with internal structure and the need for new data analysis methods. The focus of database users has shifted from

simple queries to complex analyses of the data, known as knowledge discovery in databases. Important

tasks in this area are the grouping of data objects (clustering), the classification of new data objects or the

detection of exceptional data objects (outlier detection). Most algorithms for solving those problems are based on

similarity search in databases. This makes efficient similarity search in large databases of structured objects

an important basic operation for modern database applications.

In this thesis we develop efficient methods for similarity search in large databases of

structured data and improve the efficiency of existing query processing techniques.

For the data objects, only a tree or graph structure is assumed which can be extended with arbitrary attribute

information.

Starting with an analysis of the demands from two example applications, several important requirements for

similarity measures are identified. One aspect is the adaptability of the similarity search method to the

requirements of the user and the application domain. This can even imply a change of the similarity measure

between two successive queries of the same user. An explanation component which makes clear why objects are considered

similar by the system is a necessary precondition for a purposeful adaption of the measure. Consequently,

the edit distance, well-known from string processing, is a common similarity measure for graph structured

objects. Its feature to allow a visualization of corresponding substructures and the possibility to weight

single operations are the reason for this popularity.

But it turns out that the edit distance and similar measures for tree structures are computationally extremely

complex which makes them unsuitable for today's large and even growing databases. Therefore, we develop a

multi-step query processing architecture which reduces the number of necessary distance calculations significantly.

This is achieved by employing suitable filter methods.

Furthermore, we show that by easing certain restrictions

on the similarity measure, a significant performance gain can be obtained without reducing the quality of the

measure. To achieve this, matchings of substructures (vertices or edges) of the data objects are determined.

An additional cost function for those matchings allows to derive a similarity measure for structured data, called

the edge matching distance, from

the cost optimal matching of the substructures. But even for this new similarity measure, efficiency can be improved

significantly by using a multi-step query processing approach. This allows the use of the edge matching distance for

knowledge discovery applications in large databases. Within the thesis, the properties of our new similarity search methods

are proved both theoretically and through experiments.

Multicategorical regression models are an established tool in statistical data analysis. The present thesis extends common parametric regression models for nominal and ordinal responses to more flexible nonparametric approaches. In order to obtain a flexible form of the functional effects of metrically scaled covariates, expansions in basis functions are used. The resulting predictor allows parameter estimation within the framework of multivariate generalized linear models. Estimates are obtained by maximizing a penalized likelihood with discrete penalty terms restricting the variation of estimated smooth effects.

As a result of theoretical considerations, P-Splines seem to be the ideal alternative for applying penalized basis function approaches. Based on this result, nonparametric extensions of the multinomial logit model for nominal and the cumulative logit model for ordinal responses are derived. An important feature of the proposed multinomial logit model is the distinction between global and category-specific variables. Variables of both types may enter the model in a linear form or as unspecified smooth functions. For cumulative logit models the penalization concept adopted from P-Splines is used to restrict category-specific parameters in adjacent categories. Penalization across response categories ensures availability of estimates when common estimation procedures fail to converge, so that tests for proportional odds may be performed even for critical settings. Additionally, penalties across response categories are taken into account as fixed methodical parts when fitting semiparametric partial proportional odds models.

Local smoothing methods are a widely used tool in the context of nonparametric regression. The essential idea is to perform a linear or polynomial regression locally in a neighborhood of the target point. This method is generalized in two ways. Firstly, the polynomials are substituted by arbitrary smooth basis functions, and secondly, the estimating methodology, which is based on the least squares method, is modified in a suitable way. It appears that the first concept is useful for bias reduction, while the second one is interesting for robustifcation against outliers in the predictors. As by-products some interesting relations to other mathematical and statistical topics are unveiled, concerning in particular the theorems from Taylor and Horvitz-Thompson.

In the further course of the thesis the interest turns to some particular problems which have not been a domain of local methods so far. It turns out that local smoothing methods, suitably combined, are useful for the online monitoring of time series in order to detect sudden breaks or jumps. Finally, the restriction of modelling only functional data is abandoned and a new approach to calculate principal curves, i.e. smooth curves which pass through the ``middle'' of a multidimensional, possibly multiply branched, data cloud, is developed.

This thesis is concerned with the analysis of data for a finite set of spatially structured units. For example, irregular structures, like political maps, are considered as well as regular lattices. The main field of application is geographical epidemiology.

In this thesis a prior model for the use within a hierarchical Bayesian framework is developed, and a theoretical basis is given. The proposed partition model combines the units under investigation to clusters, and allows for the estimation of parameters on the basis of local information. Special emphasis is on spatially adaptive smoothing of the data that retains possible edges in the estimated surface. Information about the existence of such edges is extracted from the data.

The investigation of different data types supports the suitability of the model for a wide range of applications. The model seems to be very flexible and shows the desired smoothing behavior. In comparison to commonly used Markov random field models the proposed model has some advantages. With respect to the quality of the data, either both models yield similar results, or the proposed model provides more clear structure in the estimates and simplifies the interpretation of the results.

This thesis aims at exploring the scopes and limits of techniques

for extracting programs from proofs. We focus on constructive

theories of inductive definitions and classical systems allowing

choice principles. Special emphasis is put on optimizations that

allow for the extraction of realistic programs.

Our main field of application is infinitary combinatorics. Higman's

Lemma, having an elegant non-constructive proof due to Nash-Williams,

constitutes an interesting case for the problem of discovering the

constructive content behind a classical proof. We give two distinct

solutions to this problem. First, we present a proof of Higman's

Lemma for an arbitrary alphabet in a theory of inductive

definitions. This proof may be considered as a constructive

counterpart to Nash-Williams' minimal-bad-sequence proof. Secondly,

using a refined $A$-translation method, we directly transform the

classical proof into a constructive one and extract a program. The

crucial point in the latter is that we do not need to avoid the axiom

of classical dependent choice but directly assign a realizer to its

translation.

A generalization of Higman's Lemma is Kruskal's Theorem.

We present a constructive proof of Kruskal's Theorem that is

completely formalized in a theory of inductive definitions.

As a practical part, we show that these methods can be carried out in

an interactive theorem prover. Both approaches to Higman's Lemma have

been implemented in Minlog.

Categorizing continuous variables arises as an important task in statistical analysis, especially in analyzing dose-response relationships. Creating meaningful groups of the predictor variables regarding the outcome variable is desirable in many settings, especially if the form of the relationship is unknown. However it is not always obvious how many groups should be build and where the cutpoints should be placed. Usually more than one explanatory variable has to be included in the analysis, and therefore one has to apply an appropriate statistical model. For this purpose we need a simple approach to model the data without many requirements. Another important issue in statistical analysis and especially in toxicology studies is proving a dose response relationship: increasing response probability with increasing predictor variable. This theses deals with cases where categorization of numerical or categorical predictor variables results as an effect of the dose-response relationship.

Isotonic regression is an alternative proposal when one wishes to establish a dose-response relationship, categorize continuous variables and estimate threshold values. The only assumption for this approach is the monotonicity in the response variable. The isotonic regression summarizes the description of n observations to l categories (level sets or solution blocks) by automatically splitting the predictor in constant risk groups. The result is always a step function, and therefore the isotonic regression can be used to fit a changepoint model. The Pooled Adjacent Violators Algorithm (PAVA) is used to fit the data.

In relation to model fitting and testing, some problems arise when the response is binary, and in the present work the difficulties are highlighted and some proposals to solve them are given. Regarding isotonic regression and binary response, the isotonic test for trend, the reduced isotonic model, multidimensional isotonic models and methods to assess threshold limit values are discussed.

The isotonic framework provides a reliable test for trend which unlike other widely used tests (the Cochran-Armitage test for example) is independent of any monotonic transformation of the dose variable and does not assume a linear shape. However the proposed large sample approximation (a weighted chi-square distribution) does not hold when the overall response probability is less than 5\% and thus exact methods are proposed in order to assess the correct p-value. In a simulation study it has been shown that the isotonic likelihood ratio test is more powerful than the Cochran-Armitage test, the Wilcoxon test and the Iso-chi-squared test.

The model resulting from PAVA can become more parsimonious if the level sets which correspond to a non significant change for the response variable are eliminated. This model is called reduced isotonic regression. That can be accomplished by two means: a sequence of Fisher tests for the adjacent 2x2 tables or the application of a variation of a "closed testing" procedure. The correction for multiple comparisons is made for the first method by an a-priori estimation of the overall significance level in a permutation procedure. In the second method the control for the expense of the type I error is effected by the closure principal. To select between full isotonic and reduced model, a procedure based on parametric bootstrap is proposed. A simulation study proved that when the maximal coefficient of determination for the analyzed data set is at least 50% and the data can be represented by a step function, the reduced monotonic regression controls successfully the trade off between model complexity and goodness of fit.

When more than one predictor is to be taken into account an additive isotonic model can be applied. Alternatively, an isotonic-surfaces model is proposed. This can be estimated by an iterative version of the Pooled Adjacent Violators Algorithm. The result is a sequence of surfaces which is mo