KLUEDO RSS FeedKLUEDO Dokumente/documents
https://kluedo.ub.uni-kl.de/index/index/
Wed, 26 Jul 2017 12:29:44 +0200Wed, 26 Jul 2017 12:29:44 +0200Time-resolved pump-probe action spectroscopy on isolated organic dyes and supramolecular photocatalysts
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4696
Dimitri Imanbaewdoctoralthesishttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4696Wed, 26 Jul 2017 12:29:44 +0200Continuous-Time Portfolio Optimization under Partial Information and Convex Constraints: Deriving Explicit Results
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4687
In this thesis we explicitly solve several portfolio optimization problems in a very realistic setting. The fundamental assumptions on the market setting are motivated by practical experience and the resulting optimal strategies are challenged in numerical simulations.
We consider an investor who wants to maximize expected utility of terminal wealth by trading in a high-dimensional financial market with one riskless asset and several stocks.
The stock returns are driven by a Brownian motion and their drift is modelled by a Gaussian random variable. We consider a partial information setting, where the drift is unknown to the investor and has to be estimated from the observable stock prices in addition to some analyst’s opinion as proposed in [CLMZ06]. The best estimate given these observations is the well known Kalman-Bucy-Filter. We then consider an innovations process to transform the partial information setting into a market with complete information and an observable Gaussian drift process.
The investor is restricted to portfolio strategies satisfying several convex constraints.
These constraints can be due to legal restrictions, due to fund design or due to client's specifications. We cover in particular no-short-selling and no-borrowing constraints.
One popular approach to constrained portfolio optimization is the convex duality approach of Cvitanic and Karatzas. In [CK92] they introduce auxiliary stock markets with shifted market parameters and obtain a dual problem to the original portfolio optimization problem that can be better solvable than the primal problem.
Hence we consider this duality approach and using stochastic control methods we first solve the dual problems in the cases of logarithmic and power utility.
Here we apply a reverse separation approach in order to obtain areas where the corresponding Hamilton-Jacobi-Bellman differential equation can be solved. It turns out that these areas have a straightforward interpretation in terms of the resulting portfolio strategy. The areas differ between active and passive stocks, where active stocks are invested in, while passive stocks are not.
Afterwards we solve the auxiliary market given the optimal dual processes in a more general setting, allowing for various market settings and various dual processes.
We obtain explicit analytical formulas for the optimal portfolio policies and provide an algorithm that determines the correct formula for the optimal strategy in any case.
We also show optimality of our resulting portfolio strategies in different verification theorems.
Subsequently we challenge our theoretical results in a historical and an artificial simulation that are even closer to the real world market than the setting we used to derive our theoretical results. However, we still obtain compelling results indicating that our optimal strategies can outperform any benchmark in a real market in general.Christian Vonwirthdoctoralthesishttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4687Fri, 21 Jul 2017 09:35:46 +0200Measuring Accountability in Nonprofit Organizations: The Impact of Nonprofit Governance on Accountability
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4683
As there is a rising interest in accountability issues and governance in nonprofit organizations,
this work aims to give some notions on the context of these two topics. Hence,
within this work, a theoretical framework is developed, whereby the correlation of accountability
and governance in nonprofit organizations shall be measured. This framework
suggests, that in nonprofit organizations, nonprofit governance, represented by
board members and professionals, has an influence on compliance, as a component of
accountability. In respect to the board members, it is supposed that, board competence,
transparency, stakeholder relationship and (public) trust are positively related to compliance.
Furthermore, it is assumed, referring to professionals, that the variables performance,
training or development and satisfaction are positively and empowerment is
negatively correlated with compliance. These assumptions are based on a thorough theoretical
literature research. Furthermore, a questionnaire is designed to measure the correlations.
This questionnaire will be amplified in a discussion following to the explanation
of the research model. Concluding, some limitations on the research model are given,
which should be taken into account by undertaking the questionnaire. Sophie Mentges; Elena Klugotherhttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4683Thu, 20 Jul 2017 09:32:03 +0200Complete Functional Verification
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4680
The dissertation describes a practically proven, particularly efficient approach for the verification of digital circuit designs. The approach outperforms simulation based verification wrt. final circuit quality as well as wrt. required verification effort. In the dissertation, the paradigm of transaction based verification is ported from simulation to formal verification. One consequence is a particular format of formal properties, called operation properties. Circuit descriptions are verified by proof of operation properties with Interval Property Checking (IPC), a particularly strong SAT based formal verification algorithm. Furtheron, a completeness checker is presented that identifies all verification gaps in sets of operation properties. This completeness checker can handle the large operation properties that arise, if this approach is applied to realistic circuits. The methodology of operation properties, Interval Property Checking, and the completeness checker form a symbiosis that is of particular benefit to the verification of digital circuit designs. On top of this symbiosis an approach to completely verify the interaction of completely verified modules has been developed by adaptation of the modelling theories of digital systems. The approach presented in the dissertation has proven in multiple commercial application projects that it indeed completely verifies modules. After reaching a termination criterion that is well defined by completeness checking, no further bugs were found in the verified modules. The approach is marketed by OneSpin Solutions GmbH, Munich, under the names "Operation Based Verification" and "Gap Free Verification".Joerg Bormannotherhttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4680Tue, 11 Jul 2017 08:36:42 +0200The Split tree for option pricing
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4677
In this dissertation convergence of binomial trees for option pricing is investigated. The focus is on American and European put and call options. For that purpose variations of the binomial tree model are reviewed.
In the first part of the thesis we investigated the convergence behavior of the already known trees from the literature (CRR, RB, Tian and CP) for the European options. The CRR and the RB tree suffer from irregular convergence, so our first aim is to find a way to get the smooth convergence. We first show what causes these oscillations. That will also help us to improve the rate of convergence. As a result we introduce the Tian and the CP tree and we proved that the order of convergence for these trees is \(O \left(\frac{1}{n} \right)\).
Afterwards we introduce the Split tree and explain its properties. We prove the convergence of it and we found an explicit first order error formula. In our setting, the splitting time \(t_{k} = k\Delta t\) is not fixed, i.e. it can be any time between 0 and the maturity time \(T\). This is the main difference compared to the model from the literature. Namely, we show that the good properties of the CRR tree when \(S_{0} = K\) can be preserved even without this condition (which is mainly the case). We achieved the convergence of \(O \left(n^{-\frac{3}{2}} \right)\) and we typically get better results if we split our tree later.Merima Nurkanovićdoctoralthesishttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4677Fri, 30 Jun 2017 13:34:19 +0200Mathematical modelling of interacting fibre structures and non-woven materials
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4675
Non–woven materials consist of many thousands of fibres laid down on a conveyor belt
under the influence of a turbulent air stream. To improve industrial processes for the
production of non–woven materials, we develop and explore novel mathematical fibre and
material models.
In Part I of this thesis we improve existing mathematical models describing the fibres on the
belt in the meltspinning process. In contrast to existing models, we include the fibre–fibre
interaction caused by the fibres’ thickness which prevents the intersection of the fibres and,
hence, results in a more accurate mathematical description. We start from a microscopic
characterisation, where each fibre is described by a stochastic functional differential
equation and include the interaction along the whole fibre path, which is described by a
delay term. As many fibres are required for the production of a non–woven material, we
consider the corresponding mean–field equation, which describes the evolution of the fibre
distribution with respect to fibre position and orientation. To analyse the particular case of
large turbulences in the air stream, we develop the diffusion approximation which yields a
distribution describing the fibre position. Considering the convergence to equilibrium on
an analytical level, as well as performing numerical experiments, gives an insight into the
influence of the novel interaction term in the equations.
In Part II of this thesis we model the industrial airlay process, which is a production method
whereby many short fibres build a three–dimensional non–woven material. We focus on
the development of a material model based on original fibre properties, machine data and
micro computer tomography. A possible linking of these models to other simulation tools,
for example virtual tensile tests, is discussed.
The models and methods presented in this thesis promise to further the field in mathematical
modelling and computational simulation of non–woven materials.Christian Nesslerdoctoralthesishttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4675Thu, 29 Jun 2017 13:34:39 +0200A measurement method for characterising micro lead on ground shaft surfaces
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4674
The detection and characterisation of undesired lead structures on shaft surfaces is a concern in production and quality control of rotary shaft lip-type sealing systems. The potential lead structures are generally divided into macro and micro lead based on their characteristics and formation. Macro lead measurement methods exist and are widely applied. This work describes a method to characterise micro lead on ground shaft surfaces. Micro lead is known as the deviation of main orientation of the ground micro texture from circumferential direction. Assessing the orientation of microscopic structures with arc minute accuracy with regard to circumferential direction requires exact knowledge of both the shaft’s orientation and the direction of surface texture. The shaft’s circumferential direction is found by calibration. Measuring systems and calibration procedures capable of calibrating shaft axis orientation with high accuracy and low uncertainty are described. The measuring systems employ areal-topographic measuring instruments suited for evaluating texture orientation. A dedicated evaluation scheme for texture orientation is based on the Radon transform of these topographies and parametrised for the application. Combining the calibration of circumferential direction with the evaluation of texture orientation the method enables the measurement of micro lead on ground shaft surfaces.Philipp Arneckedoctoralthesishttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4674Tue, 27 Jun 2017 12:24:37 +0200Product Pricing with Additive Influences - Algorithms and Complexity Results for Pricing in Social Networks
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4662
We introduce and investigate a product pricing model in social networks where the value a possible buyer assigns to a product is influenced by the previous buyers. The selling proceeds in discrete, synchronous rounds for some set price and the individual values are additively altered. Whereas computing the revenue for a given price can be done in polynomial time, we show that the basic problem PPAI, i.e., is there a price generating a requested revenue, is weakly NP-complete. With algorithm Frag we provide a pseudo-polynomial time algorithm checking the range of prices in intervals of common buying behavior we call fragments. In some special cases, e.g., solely positive influences, graphs with bounded in-degree, or graphs with bounded path length, the amount of fragments is polynomial. Since the run-time of Frag is polynomial in the amount of fragments, the algorithm itself is polynomial for these special cases. For graphs with positive influence we show that every buyer does also buy for lower prices, a property that is not inherent for arbitrary graphs. Algorithm FixHighest improves the run-time on these graphs by using the above property.
Furthermore, we introduce variations on this basic model. The version of delaying the propagation of influences and the awareness of the product can be implemented in our basic model by substituting nodes and arcs with simple gadgets. In the chapter on Dynamic Product Pricing we allow price changes, thereby raising the complexity even for graphs with solely positive or negative influences. Concerning Perishable Product Pricing, i.e., the selling of products that are usable for some time and can be rebought afterward, the principal problem is computing the revenue that a given price can generate in some time horizon. In general, the problem is #P-hard and algorithm Break runs in pseudo-polynomial time. For polynomially computable revenue, we investigate once more the complexity to find the best price.
We conclude the thesis with short results in topics of Cooperative Pricing, Initial Value as Parameter, Two Product Pricing, and Bounded Additive Influence. Florian David Schwahndoctoralthesishttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4662Fri, 23 Jun 2017 11:37:27 +0200An Integer Network Flow Problem with Bridge Capacities
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4667
In this paper a modified version of dynamic network
ows is discussed. Whereas dynamic network flows are widely analyzed already, we consider a dynamic flow problem with aggregate arc capacities called Bridge
Problem which was introduced by Melkonian [Mel07]. We extend his research to integer flows and show that this problem is strongly NP-hard. For practical relevance we also introduce and analyze the hybrid bridge problem, i.e. with underlying networks whose arc capacity can limit aggregate flow (bridge problem) or the flow entering an arc at each time (general dynamic flow). For this kind of problem we present efficient procedures for
special cases that run in polynomial time. Moreover, we present a heuristic for general hybrid graphs with restriction on the number of bridge arcs.
Computational experiments show that the heuristic works well, both on random graphs and on graphs modeling also on realistic scenarios.Horst W. Hamacher; Anika Kinscherffworkingpaperhttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4667Wed, 14 Jun 2017 10:38:36 +0200Characterization of Structures, Fragmentation Pathways and Magnetism of Mononuclear and Oligonuclear Transition Metal Complexes in Isolation
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4654
This thesis comprises several independent research studies on transition metal complexes as trapped ions in isolation. Electrospray Ionization (ESI) serves to transfer ions from solution into the gas phase for mass spectrometric investigations. Subsequently, a variety of experimental and theoretical methods provide fundamental insights into molecular properties of the isolated complexes: InfraRed (Multiple) Photon Dissociation (IR-(M)PD) spectroscopy provides information on binding motifs and molecular structures at cryo temperatures as well as at room temperature. Collision Induced Dissociation (CID) serves to elucidate molecular fragmentation pathways as well as relative stabilities of the complexes at room temperature. Quantum chemical calculations via Density Functional Theory (DFT) substantiate the experimental results and deepen the fundamental insights into the molecular properties of the complexes. Magnetic couplings between metal centers in oligonuclear complexes are investigated by Broken Symmetry DFT modelling and X Ray Magnetic Circular Dichroism (XMCD) spectroscopy.Johannes Langdoctoralthesishttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4654Wed, 24 May 2017 15:57:40 +0200Convex Analysis for Processing Hyperspectral Images and Data from Hadamard Spaces
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4650
This thesis brings together convex analysis and hyperspectral image processing.
Convex analysis is the study of convex functions and their properties.
Convex functions are important because they admit minimization by efficient algorithms
and the solution of many optimization problems can be formulated as
minimization of a convex objective function, extending much beyond
the classical image restoration problems of denoising, deblurring and inpainting.
\(\hspace{1mm}\)
At the heart of convex analysis is the duality mapping induced within the
class of convex functions by the Fenchel transform.
In the last decades efficient optimization algorithms have been developed based
on the Fenchel transform and the concept of infimal convolution.
\(\hspace{1mm}\)
The infimal convolution is of similar importance in convex analysis as the
convolution in classical analysis. In particular, the infimal convolution with
scaled parabolas gives rise to the one parameter family of Moreau-Yosida envelopes,
which approximate a given function from below while preserving its minimum
value and minimizers.
The closely related proximal mapping replaces the gradient step
in a recently developed class of efficient first-order iterative minimization algorithms
for non-differentiable functions. For a finite convex function,
the proximal mapping coincides with a gradient step of its Moreau-Yosida envelope.
Efficient algorithms are needed in hyperspectral image processing,
where several hundred intensity values measured in each spatial point
give rise to large data volumes.
\(\hspace{1mm}\)
In the \(\textbf{first part}\) of this thesis, we are concerned with
models and algorithms for hyperspectral unmixing.
As part of this thesis a hyperspectral imaging system was taken into operation
at the Fraunhofer ITWM Kaiserslautern to evaluate the developed algorithms on real data.
Motivated by missing-pixel defects common in current hyperspectral imaging systems,
we propose a
total variation regularized unmixing model for incomplete and noisy data
for the case when pure spectra are given.
We minimize the proposed model by a primal-dual algorithm based on the
proximum mapping and the Fenchel transform.
To solve the unmixing problem when only a library of pure spectra is provided,
we study a modification which includes a sparsity regularizer into model.
\(\hspace{1mm}\)
We end the first part with the convergence analysis for a multiplicative
algorithm derived by optimization transfer.
The proposed algorithm extends well-known multiplicative update rules
for minimizing the Kullback-Leibler divergence,
to solve a hyperspectral unmixing model in the case
when no prior knowledge of pure spectra is given.
\(\hspace{1mm}\)
In the \(\textbf{second part}\) of this thesis, we study the properties of Moreau-Yosida envelopes,
first for functions defined on Hadamard manifolds, which are (possibly) infinite-dimensional
Riemannian manifolds with negative curvature,
and then for functions defined on Hadamard spaces.
\(\hspace{1mm}\)
In particular we extend to infinite-dimensional Riemannian manifolds an expression
for the gradient of the Moreau-Yosida envelope in terms of the proximal mapping.
With the help of this expression we show that a sequence of functions
converges to a given limit function in the sense of Mosco
if the corresponding Moreau-Yosida envelopes converge pointwise at all scales.
\(\hspace{1mm}\)
Finally we extend this result to the more general setting of Hadamard spaces.
As the reverse implication is already known, this unites two definitions of Mosco convergence
on Hadamard spaces, which have both been used in the literature,
and whose equivalence has not yet been known.Martin J. Montagdoctoralthesishttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4650Mon, 22 May 2017 11:26:42 +0200Urban Quality of Life at Risk
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4646
Urban quality of life is currently conceptualized in principally economic terms. As the decline in manufacturing activities, the rise of the service and knowledge economy, the growing importance of accessibility and globalizing processes continue to reconfigure the economic competition between cities, quality of life enters the discourse primarily as a means to attract high-skilled workers and improve the city’s economic prospects. Local governments increasingly seek partnerships with local and foreign capital, reorganizing institutions and tasks to attract capital, including the “selling of place”, strengthening place promotion and marketing efforts. The rhetoric clearly welcomes wealthy, creative, high-skilled people, disadvantaged and low skilled groups receive less attention in the making of places. Especially with respect to inner city areas, high quality of life is promoted as spaces for ‘clean’ and convenient consumption with positive atmospheres and shiny images.
Yet, a plethora of theoretical engagements with urban everyday live reminds us that, while on the one hand, variety of jobs, quality of public spaces, range of shops and services, cultural facilities and public transport are important place characteristics, more subjective aspects such as safe neighbourhoods, well-being, community prospects, social cohesion, happiness, satisfaction and social and spatial justice are equally crucial determinants of urban quality of life. These elements of urban quality of life – and how they are experienced by diverse formations of urban inhabitants – seem to be absent from, if not at odds with, the dominant discourse in rankings, policy and practice. Urban life, social cohesion and complexity are at risk in the dynamics of modernization and adaptation strategies of cities. Gentrification, the occupation of inner-city districts by hyper-rich people, segregation and displacement of lower and middle classes can be observed as a consequence of these long-lasting strategies.
Well-known sociologists and geographers from the UK and Germany have presented their insights on the matter and debate theoretical and empirical attempts to capture the dynamics of urban processes in shaping the quality of life.
Annette Spellerberg; Maren Harnackbookhttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4646Fri, 19 May 2017 14:36:45 +0200Coverage of Compositional Property Sets for Hardware and Hardware-dependent Software in Formal System-on-Chip Verification
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4640
Divide-and-Conquer is a common strategy to manage the complexity of system design and verification. In the context of System-on-Chip (SoC) design verification, an SoC system is decomposed into several modules and every module is separately verified. Usually an SoC module is reactive: it interacts with its environmental modules. This interaction is normally modeled by environment constraints, which are applied to verify the SoC module. Environment constraints are assumed to be always true when verifying the individual modules of a system. Therefore the correctness of environment constraints is very important for module verification.
Environment constraints are also very important for coverage analysis. Coverage analysis in formal verification measures whether or not the property set fully describes the functional behavior of the design under verification (DuV). if a set of properties describes every functional behavior of a DuV, the set of properties is called complete. To verify the correctness of environment constraints, Assume-Guarantee Reasoning rules can be employed.
However, the state of the art assume-guarantee reasoning rules cannot be applied to the environment constraints specified by using an industrial standard property language such as SystemVerilog Assertions (SVA).
This thesis proposes a new assume-guarantee reasoning rule that can be applied to environment constraints specified by using a property language such as SVA. In addition, this thesis proposes two efficient plausibility checks for constraints that can be conducted without a concrete implementation of the considered environment.
Furthermore, this thesis provides a compositional reasoning framework determining that a system is completely verified if all modules are verified with Complete Interval Property Checking (C-IPC) under environment constraints.
At present, there is a trend that more of the functionality in SoCs is shifted from the hardware to the hardware-dependent software (HWDS), which is a crucial component in an SoC, since other software layers, such as the operating systems are built on it. Therefore there is an increasing need to apply formal verification to HWDS, especially for safety-critical systems.
The interactions between HW and HWDS are often reactive, and happen in a temporal order. This requires new property languages to specify the reactive behavior at the HW and SW interfaces.
This thesis introduces a new property language, called Reactive Software Property Language (RSPL), to specify the reactive interactions between the HW and the HWDS.
Furthermore, a method for checking the completeness of software properties, which are specified by using RSPL, is presented in this thesis. This method is motivated by the approach of checking the completeness of hardware properties.
Binghao Baodoctoralthesishttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4640Thu, 11 May 2017 12:41:38 +0200Small self-centralizing subgroups in defect groups of finite classical groups
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4617
In this thesis, we consider a problem from modular representation theory of finite groups. Lluís Puig asked the question whether the order of the defect groups of a block \( B \) of the group algebra of a given finite group \( G \) can always be bounded in terms of the order of the vertices of an arbitrary simple module lying in \( B \).
In characteristic \( 2 \), there are examples showing that this is not possible in general, whereas in odd characteristic, no such examples are known. For instance, it is known that the answer to Puig's question is positive in case that \( G \) is a symmetric group, by work of Danz, Külshammer, and Puig.
Motivated by this, we study the cases where \( G \) is a finite classical group in non-defining characteristic or one of the finite groups \( G_2(q) \) or \( ³D_4(q) \) of Lie type, again in non-defining characteristic. Here, we generalize Puig's original question by replacing the vertices occurring in his question by arbitrary self-centralizing subgroups of the defect groups. We derive positive and negative answers to this generalized question.
\[\]
In addition to that, we determine the vertices of the unipotent simple \( GL_2(q) \)-module labeled by the partition \( (1,1) \) in characteristic \( 2 \). This is done using a method known as Brauer construction.Pablo Lukadoctoralthesishttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4617Thu, 16 Mar 2017 08:27:05 +0100Analysis and Verification of Complex Robot Systems using Behaviour-Based Control
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4616
The development of autonomous mobile robots is a major topic of current research. As those robots must be able to react to changing environments and avoid collisions also with moving obstacles, the fulfilment of safety requirements is an important aspect. Behaviour-based systems (BBS) have proven to meet several of the properties required for these kindsof robots, such as reactivity, extensibility and re-usability of individual components. BBS consist of a number of behavioural components that individually realise simple tasks. Their interconnection allows to achieve complex robot behaviour, which implies that correct
connections are crucial. The resulting networks can get very large making them difficult to verify. This dissertation presents a novel concept for the analysis and verification of complex autonomous robot systems controlled by behaviour-based software architectures with special focus on the integration of environmental aspects into the processes.
Several analysis techniques have been investigated and adapted to the special requirements of BBS. These include a structural analysis, which is used to find constraint violations and faults in the network layout. Fault tree analysis is applied to identify root causes of hazards and the relationship of system events. For this, a technique to map the behaviour-based control network to the structure of a fault tree has been developed. Testing and data analysis are used for the detection of failures and their root causes. Here, a new concept that identifies patterns in data recorded during test runs has been introduced.
All of these methods cannot guarantee failure-free and safe robot behaviour and can never prove the absence of failures. Therefore, model checking as formal verification technique that proves a property to be correct for the given system, has been chosen to complement the set of analysis techniques. A novel concept for the integration of environmental influences into the model checking process is proposed. Environmental situations and the sensor processing chain are represented as synchronised automata similar to the modelling of the behavioural network. Tools supporting the whole verification process including the creation of formal queries in its environment have been developed.
During the verification of large behavioural networks, the scalability of the model checking approach appears as a big problem. Several approaches that deal with this problem have been investigated and the selection of slicing and abstraction methods has been justified. A concept for the application of these methods is provided, that reduces the behavioural network to the relevant parts before the actual verification process.
All techniques have been applied to the behaviour-based control system of the autonomous outdoor robot RAVON. Its complex network with more than 400 components allows for demonstrating the soundness of the presented concepts. The set of diﬀerent techniques provides a fundamental basis for a comprehensive analysis and verification of BBS acting in changing environments.Lisa Kiekbuschdoctoralthesishttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4616Wed, 15 Mar 2017 11:52:01 +0100Analysis of Different Random Graph Models in the Identification of Network Motifs in Complex Networks
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4615
This thesis is concerned with different null-models that are used in network analysis. Whenever it is of interest whether a real-world graph is exceptional regarding a particular measure, graphs from a null-model can be used to compare the real-world graph to. By analyzing an appropriate null-model, a researcher may find whether the results of the measure on the real-world graph is exceptional or not.
Deciding which null-model to use is hard and sometimes the difference between the null-models is not even considered. In this thesis, there are several results presented: First, based on simple global measures, undirected graphs are analyzed. The results for these measures indicates that it is not important which null-model is used, thus, the fastest algorithm of a null-model may be used. Next, local measures are investigated. The fastest algorithm proves to be the most complicated to analyze. The model includes multigraphs which do not meet the conditions of all the measures, thus, the measures themselves have to be altered to take care of multigraphs as well. After careful consideration, the conditions are met and the analysis shows, that the fastest is not always the best.
The same applies for directed graphs, as is shown in the last part. There, another more complex measure on graphs is introduced. I continue testing the applicability of several null-models; in the end, a set of equations proves to be fast and good enough as long as conditions regarding the degree sequence are met.Wolfgang Schlauchdoctoralthesishttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4615Thu, 09 Mar 2017 08:54:04 +0100C-H-activation-mediated-by-Transition-Metals
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4609
C-H activations(C-H bond weakening effects) under impact of transition metal atoms are theoretically investigated, two model systems are used, one is CH3MX, the other is n-ButMX, (X=F,Cl,Br,I,H,CN, M include all transition metal atoms from group 4 to group 10). Dawei Zhaodoctoralthesishttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4609Wed, 08 Mar 2017 13:32:49 +0100Graph Coloring Applications and Defining Sets in Graph Theory
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4612
Abstract
The main theme of this thesis is about Graph Coloring Applications and Defining Sets in Graph Theory.
As in the case of block designs, finding defining sets seems to be difficult problem, and there is not a general conclusion. Hence we confine us here to some special types of graphs like bipartite graphs, complete graphs, etc.
In this work, four new concepts of defining sets are introduced:
• Defining sets for perfect (maximum) matchings
• Defining sets for independent sets
• Defining sets for edge colorings
• Defining set for maximal (maximum) clique
Furthermore, some algorithms to find and construct the defining sets are introduced. A review on some known kinds of defining sets in graph theory is also incorporated, in chapter 2 the basic definitions and some relevant notations used in this work are introduced.
chapter 3 discusses the maximum and perfect matchings and a new concept for a defining set for perfect matching.
Different kinds of graph colorings and their applications are the subject of chapter 4.
Chapter 5 deals with defining sets in graph coloring. New results are discussed along with already existing research results, an algorithm is introduced, which enables to determine a defining set of a graph coloring.
In chapter 6, cliques are discussed. An algorithm for the determination of cliques using their defining sets. Several examples are included.
Masoumeh Ahadi Moghaddamdoctoralthesishttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4612Mon, 06 Mar 2017 14:35:31 +0100Portfolio Optimization with Risk Constraints in the View of Stochastic Interest Rates
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4602
We discuss the portfolio selection problem of an investor/portfolio manager in an arbitrage-free financial market where a money market account, coupon bonds and a stock are traded continuously. We allow for stochastic interest rates and in particular consider one and two-factor Vasicek models for the instantaneous
short rates. In both cases we consider a complete and an incomplete market setting by adding a suitable number of bonds.
The goal of an investor is to find a portfolio which maximizes expected utility
from terminal wealth under budget and present expected short-fall (PESF) risk
constraints. We analyze this portfolio optimization problem in both complete and
incomplete financial markets in three different cases: (a) when the PESF risk is
minimum, (b) when the PESF risk is between minimum and maximum and (c) without risk constraints. (a) corresponds to the portfolio insurer problem, in (b) the risk constraint is binding, i.e., it is satisfied with equality, and (c) corresponds
to the unconstrained Merton investment.
In all cases we find the optimal terminal wealth and portfolio process using the
martingale method and Malliavin calculus respectively. In particular we solve in the incomplete market settings the dual problem explicitly. We compare the
optimal terminal wealth in the cases mentioned using numerical examples. Without
risk constraints, we further compare the investment strategies for complete
and incomplete market numerically.William Ntambaradoctoralthesishttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4602Wed, 01 Mar 2017 08:14:31 +0100Asymptotics for change-point tests and change-point estimators
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4599
In change-point analysis the point of interest is to decide if the observations follow one model
or if there is at least one time-point, where the model has changed. This results in two sub-
fields, the testing of a change and the estimation of the time of change. This thesis considers
both parts but with the restriction of testing and estimating for at most one change-point.
A well known example is based on independent observations having one change in the mean.
Based on the likelihood ratio test a test statistic with an asymptotic Gumbel distribution was
derived for this model. As it is a well-known fact that the corresponding convergence rate is
very slow, modifications of the test using a weight function were considered. Those tests have
a better performance. We focus on this class of test statistics.
The first part gives a detailed introduction to the techniques for analysing test statistics and
estimators. Therefore we consider the multivariate mean change model and focus on the effects
of the weight function. In the case of change-point estimators we can distinguish between
the assumption of a fixed size of change (fixed alternative) and the assumption that the size
of the change is converging to 0 (local alternative). Especially, the fixed case in rarely analysed
in the literature. We show how to come from the proof for the fixed alternative to the
proof of the local alternative. Finally, we give a simulation study for heavy tailed multivariate
observations.
The main part of this thesis focuses on two points. First, analysing test statistics and, secondly,
analysing the corresponding change-point estimators. In both cases, we first consider a
change in the mean for independent observations but relaxing the moment condition. Based on
a robust estimator for the mean, we derive a new type of change-point test having a randomized
weight function. Secondly, we analyse non-linear autoregressive models with unknown
regression function. Based on neural networks, test statistics and estimators are derived for
correctly specified as well as for misspecified situations. This part extends the literature as
we analyse test statistics and estimators not only based on the sample residuals. In both
sections, the section on tests and the one on the change-point estimator, we end with giving
regularity conditions on the model as well as the parameter estimator.
Finally, a simulation study for the case of the neural network based test and estimator is
given. We discuss the behaviour under correct and mis-specification and apply the neural
network based test and estimator on two data sets.Stefanie Schwaardoctoralthesishttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4599Tue, 28 Feb 2017 13:18:02 +0100Having a Plan B for Robust Optimization
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4585
We extend the standard concept of robust optimization by the introduction of an alternative solution. In contrast to the classic concept, one is allowed to chose two solutions from which the best can be picked after the uncertain scenario has been revealed. We focus in this paper on the resulting robust problem for combinatorial problems with bounded uncertainty sets. We present a reformulation of the robust problem which decomposes it into polynomially many subproblems. In each subproblem one needs to find two solutions which are connected by a cost function which penalizes if the same element is part of both solutions. Using this reformulation, we show how the robust problem can be solved efficiently for the unconstrained combinatorial problem, the selection problem, and the minimum spanning tree problem. The robust problem corresponding to the shortest path problem turns out to be NP-complete on general graphs. However, for series-parallel graphs, the robust shortest path problem can be solved efficiently. Further, we show how approximation algorithms for the subproblem can be used to compute approximate solutions for the original problem.André Chasseinpreprinthttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4585Wed, 22 Feb 2017 14:40:39 +0100How Entrepreneurs Develop and Influence their Employees
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4584
This dissertation explores how entrepreneurs develop their employees to qualify them for their tasks in entrepreneurial firms, and analyzes in what way effectuation and entrepreneurial passion determine how entrepreneurs influence their employees.Sylvia Hubnerdoctoralthesishttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4584Thu, 16 Feb 2017 09:31:23 +0100Formal Verification of Firmware-Based System-on-Chip Modules
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4567
In current practices of system-on-chip (SoC) design a trend can be observed to integrate more and more low-level software components into the system hardware at different levels of granularity. The implementation of important control functions and communication structures is frequently shifted from the SoC’s hardware into its firmware. As a result, the tight coupling of hardware and software at a low level of granularity raises substantial verification challenges since the conventional practice of verifying hardware and software independently is no longer sufficient. This calls for new methods for verification based on a joint analysis of hardware and software.
This thesis proposes hardware-dependent models of low-level software for performing formal verification. The proposed models are conceived to represent the software integrated with its hardware environment according to the current SoC design practices. Two hardware/software integration scenarios are addressed in this thesis, namely, speed-independent communication of the processor with its hardware periphery and cycle-accurate integration of firmware into an SoC module. For speed-independent hardware/software integration an approach for equivalence checking of hardware-dependent software is proposed and an evaluated. For the case of cycle-accurate hardware/software integration, a model for hardware/software co-verification has been developed and experimentally evaluated by applying it to property checking.Carlos Villarragadoctoralthesishttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4567Tue, 31 Jan 2017 13:39:07 +0100Usability of polymer film heat exchangers in the chemical industry
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4563
The main goal of this work was the study of the applicability of a polymer film heat exchanger concept for the applications in the chemical industry, such as the condensation of organic solvents. The polymer film heat exchanger investigated is a plate heat exchanger with very thin (0.025 – 0.1 mm) plates or films, which separate the fluids and enable the heat transfer. After a successful application of this concept to seawater desalination in a previous work, a further step is in chemical engineering, where the good chemical resistance of polymers in aggressive fluids is the challenge.
Two approaches were performed in this work. The first one was experimental and included the study of the chemical and mechanical resistance of preselected films, made of polymer materials, such as polyimide (PI), polyethylene terephthalate (PET) and polytetrafluoroethylene (PTFE). To simulate realistic operating conditions in a heat exchanger the films were exposed to a combined thermal (up to 90°C) and mechanical pressure loads (4-6 bar) with permanent contact with the relevant organic solvents, such as toluene, hexane, heptane and tetrahydrofuran (THF). Furthermore, a lab-scale apparatus and a full-scale demonstrator were manufactured in cooperation with two industrial partners. These were used for the investigation of the heat transfer performance for operating modes with and without phase change.
In addition to the experimental work, a coupled finite element –computational fluid dynamics (FEM-CFD)-model was developed, based on the fluid-structure-interaction (FSI). Two major tasks had to be solved here. The first one was the modelling of the condensation process, based on available mathematical models and energy balances. The second one was the consideration of the partially reversible deformation of the used film during operation. Since this deformation changes the geometry of the fluid channels also has an influence on the overall performance of the apparatus, a coupled FEM-CFD model was developed.
During the experimental study of the chemical resistance of the films, the PTFE film showed the best performance, and hence can be used for all four tested solvents. For the polyimide film, failures while exposed to THF were observed, and the PET film can only be used with water and hexane. With the used lab-scale heat exchanger and the full-scale demonstrator competitive overall heat transfer coefficients between 270 W/m²K and 700 W/m²K could be reached for the liquid-liquid (water-water, water-hexane) operation mode without phase change. For the condensation process, overall heat transfer coefficients of up to 1700/m²K could be obtained.
The numerical approach led to a well-functioning coupled model in a very small scale (1 cm²). An upscale, however, failed due to enormous hardware resources necessary required for the simulation of the entire full-scale demonstrator. The main reason for this is the very low thickness of the films, which leads to tiny mesh element sizes (<0.05 mm) necessary to model the deformation of the film. The modelling of the liquid-liquid heat transfer provided an acceptable accuracy (approx. 10%), but at very low rates the deviations were then higher (over 30%). The results of the condensation modelling were ambivalent. One the one hand a physically plausible model was developed, which could map the entire condensation process. On the other hand, the corresponding energy balance revealed major inaccuracy and hence could not be used for the determination of the overall heat transfer and showed the current limits of the FEM-CFD approach.
Dmitrij Laaberdoctoralthesishttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4563Mon, 30 Jan 2017 10:53:49 +0100Magnetic Field-based Localization System
https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4558
This dissertation describes an indoor localization system based on oscillating magnetic fields and the underlying processing architecture. The system consists of several fixed anchor points, generating the magnetic fields (transmitter), and wearable magnetic field measurement units, whose position should be determined (receiver). The system is evaluated in different environments and application areas. Additionally, various fields of application are discussed and assessed in ubiquitous and pervasive computing and Ambient Assisted Living. The fusion of magnetic field-based distance information and positions derived from LIDAR distance measurements is described and evaluated.
The system architecture consists of three layers, a physical layer, a layer for position and distance estimation between a magnetic field transmitter and a receiver, and a layer which uses several measurements to different transmitters to estimate the overall position of a wearable measurement unit.
Each layer covers different aspects which have to be taken care of when magnetic field information is processed. Especially the properties of the generated magnetic field information are considered in the processing algorithms.
The physical layer covers the magnetic field generation and magnetic Field-Based information transfer, synchronization of a transmitter and the receivers and the description of the locally measured magnetic fields on the receiver side. After a transfer of this information to a central processing unit, the hardware specific signal levels are transformed to the levels of the theoretical magnetic field models. The values are then used to estimate candidate positions and distances. Due to symmetrical effects of the magnetic fields, it is only possible to reduce the receiver position to 8 points around the transmitter (one position in each of the octants of the coordinate system). The determined positions have a mean error of 108 cm, the average error of the distance is 40 cm.
On top of this, the distance and position information against different transmitters are fused, this covers clock synchronization of transmitters, triggering and scheduling sequences and distance and position based localization and tracking algorithms. The magnetic-field-based indoor localization system has been evaluated in different applications and environments; the mean position error is 60 cm to 70 cm depending on the environment. A comparison against an RF-based indoor localization system shows the robustness of magnetic fields against RF shadows caused by big metal objects.
We additionally present algorithms for regions of interest detection, working on raw magnetic field information and transformed position and distance information. Setups in larger areas can distinguish regions which are further than 50 cm apart, small scale coil setups (3 transmitters in 2m^3) allow to resolve regions below 20 cm.
In the end, we describe a fusion algorithm for a wearable localization system based on 4 LIDAR distance measurement units and magnetic field-based distance estimation. The magnetic field indoor localization system provides distance proximity information which is used to resolve ambiguous position estimates of the LIDAR system. In a room (8m × 10m), we achieve a mean error of 8 cm.Gerald Stephan Pirkldoctoralthesishttps://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/4558Wed, 25 Jan 2017 17:41:35 +0100