### Filtern

#### Erscheinungsjahr

- 2014 (142) (entfernen)

#### Dokumenttyp

- Dissertation (77)
- Preprint (28)
- Wissenschaftlicher Artikel (15)
- Teil eines Periodikums (14)
- Arbeitspapier (4)
- Sonstiges (2)
- Bericht (1)
- Studienarbeit (1)

#### Schlagworte

- Denkmäler (8)
- Monitoring (8)
- Raumplanung (8)
- Brücken (5)
- Bestandserhaltung (4)
- Zerstörungsfreie Prüfung (4)
- Multiobjective optimization (3)
- Querkraft (3)
- Zustandserfassung (3)
- Arylhydrocarbon-Rezeptor (2)

#### Fachbereich / Organisatorische Einheit

- Fachbereich Mathematik (43)
- Fachbereich Informatik (15)
- Fachbereich Maschinenbau und Verfahrenstechnik (13)
- Fachbereich Raum- und Umweltplanung (13)
- Fachbereich Sozialwissenschaften (13)
- Fachbereich Chemie (12)
- Fachbereich Bauingenieurwesen (10)
- Universität (8)
- Fachbereich Wirtschaftswissenschaften (4)
- Fachbereich Biologie (3)

Congress Report 2014.11-12
(2014)

Embedded systems, ranging from very simple systems up to complex controllers, may
nowadays have quite challenging real-time requirements. Many embedded systems are reactive
systems that have to respond to environmental events and have to guarantee certain real-time
constrain. Their execution is usually divided into reaction steps, where in each step, the
system reads inputs from the environment and reacts to these by computing corresponding
outputs.
The synchronous Model of Computation (MoC) has proven to be well-suited for the
development of reactive real-time embedded systems whose paradigm directly reflects the
reactive nature of the systems it describes. Another advantage is the availability of formal
verification by model checking as a result of the deterministic execution based on a formal
semantics. Nevertheless, the increasing complexity of embedded systems requires to compensate
the natural disadvantages of model checking that suffers from the well-known state-space
explosion problem. It is therefore natural to try to integrate other verification methods with
the already established techniques. Hence, improvements to encounter these problems are
required, e.g., appropriate decomposition techniques, which encounter the disadvantages
of the model checking approach naturally. But defining decomposition techniques for synchronous
language is a difficult task, as a result of the inherent parallelism emerging from
the synchronous broadcast communication.
Inspired by the progress in the field of desynchronization of synchronous systems by
representing them in other MoCs, this work will investigate the possibility of adapting and use
methods and tools designed for other MoC for the verification of systems represented in the
synchronous MoC. Therefore, this work introduces the interactive verification of synchronous
systems based on the basic foundation of formal verification for sequential programs – the
Hoare calculus. Due to the different models of computation several problems have to be
solved. In particular due to the large amount of concurrency, several parts of the program
are active at the same point of time. In contrast to sequential programs, a decomposition
in the Hoare-logic style that is in some sense a symbolic execution from one control flow
location to another one requires the consideration of several flows here. Therefore, different
approaches for the interactive verification of synchronous systems are presented.
Additionally, the representation of synchronous systems by other MoCs and the influence
of the representation on the verification task by differently embedding synchronous system
in a single verification tool are elaborated.
The feasibility is shown by integration of the presented approach with the established
model checking methods by implementing the AIFProver on top of the Averest system.

We consider the problem of finding efficient locations of surveillance cameras, where we distinguish
between two different problems. In the first, the whole area must be monitored and the number of cameras
should be as small as possible. In the second, the goal is to maximize the monitored area for a fixed number of
cameras. In both of these problems, restrictions on the ability of the cameras, like limited depth of view or range
of vision are taken into account. We present solution approaches for these problems and report on results of
their implementations applied to an authentic problem. We also consider a bicriteria problem with two objectives:
maximizing the monitored area and minimizing the number of cameras, and solve it for our study case.

This thesis, whose subject is located in the field of algorithmic commutative algebra and algebraic geometry, consists of three parts.
The first part is devoted to parallelization, a technique which allows us to take advantage of the computational power of modern multicore processors. First, we present parallel algorithms for the normalization of a reduced affine algebra A over a perfect field. Starting from the algorithm of Greuel, Laplagne, and Seelisch, we propose two approaches. For the local-to-global approach, we stratify the singular locus Sing(A) of A, compute the normalization locally at each stratum and finally reconstruct the normalization of A from the local results. For the second approach, we apply modular methods to both the global and the local-to-global normalization algorithm.
Second, we propose a parallel version of the algorithm of Gianni, Trager, and Zacharias for primary decomposition. For the parallelization of this algorithm, we use modular methods for the computationally hardest steps, such as for the computation of the associated prime ideals in the zero-dimensional case and for the standard bases computations. We then apply an innovative fast method to verify that the result is indeed a primary decomposition of the input ideal. This allows us to skip the verification step at each of the intermediate modular computations.
The proposed parallel algorithms are implemented in the open-source computer algebra system SINGULAR. The implementation is based on SINGULAR's new parallel framework which has been developed as part of this thesis and which is specifically designed for applications in mathematical research.
In the second part, we propose new algorithms for the computation of syzygies, based on an in-depth analysis of Schreyer's algorithm. Here, the main ideas are that we may leave out so-called "lower order terms" which do not contribute to the result of the algorithm, that we do not need to order the terms of certain module elements which occur at intermediate steps, and that some partial results can be cached and reused.
Finally, the third part deals with the algorithmic classification of singularities over the real numbers. First, we present a real version of the Splitting Lemma and, based on the classification theorems of Arnold, algorithms for the classification of the simple real singularities. In addition to the algorithms, we also provide insights into how real and complex singularities are related geometrically. Second, we explicitly describe the structure of the equivalence classes of the unimodal real singularities of corank 2. We prove that the equivalences are given by automorphisms of a certain shape. Based on this theorem, we explain in detail how the structure of the equivalence classes can be computed using SINGULAR and present the results in concise form. The probably most surprising outcome is that the real singularity type \(J_{10}^-\) is actually redundant.

Researchers and analysts in modern industrial and academic environments are faced with a daunting amount of multivariate data. While there has been significant development in the areas of data mining and knowledge
discovery, there is still the need for improved visualizations and generic solutions. The state-of-the-art in visual analytics and exploratory data visualization is to incorporate more profound analysis methods while focusing on improving interactive abilities, in order to support data analysts in gaining new insights through visual exploration and hypothesis building.
In the research field of exploratory data visualization, this thesis contributes new approaches in dimension reduction that tackle a number of shortcomings in state-of-the-art methods, such as interpretability and ambiguity. By combining methods from several disciplines, we describe how ambiguity can be countered effectively by visualizing coordinate values within a lower-dimensional embedding, thereby focusing on the display of the structural composition of high-dimensional data and on an intuitive depiction of inherent global relationships. We also describe how properties and alignment of high-dimensional manifolds can be analyzed in different levels of detail by means of a self-embedding hierarchy of local projections, each using full degree of freedom, while keeping the global context.
To the application field of air quality research, the thesis provides novel means for the research of aerosol source contributions. Triggered by this particularly challenging application problem, we instigate a new research direction in the area of visual analytics by describing a methodology to model-based visual analysis that (i) allows the scientist to be “in the loop” of computations and (ii) enables him to verify and control the analysis process, in order to steer computations towards physical meaning. Careful reflection of our work in this application has led us to derive key design choices that underlie and transcend beyond application-specific solutions. As a result, we describe a general design methodology to computing parameters of a pre-defined analytical model that map to multivariate data. Core applications areas that can benefit from our approach are within engineering disciplines, such as civil, chemical, electrical, and mechanical engineering, as well as in geology, physics, and biology.

The heart is reported to show a net consumption of lactate. This may contribute up to 15% to the total body lactate disposal. In this work, the consumption of lactate was shown for the first
time on the single cell level with the new FRET-based lactate sensor Laconic.
Research published until today, almost exclusively reports the monocarboxylate transporter 1
(MCT1) as the transporter responsible for myocardial lactate uptake. As this membrane
transporter transports lactate together with H+ in a stoichiometry of 1:1, lactate transport is
coupled to pH regulation. Consequently, interactions of MCT1 and acid/base regulating proteins
(carbonic anhydrases (CAs and sodium bicarbonate co-transporters (NBCs)) are described in
the oocyte expression system, skeletal muscle and cancer cells.
In this work it is shown that activity of extracellular CA increases lactate uptake into mouse
cardiomyocytes by 27% and lactate induced JA/B by 42.8% to 46.2%. This effect is most likely
mediated via NBC/CA interaction because inhibition of extracellular CA reduces HCO3--
dependent acid extruding JA/B by 53.3% to 78.4%. This may link lactate uptake to cellular
respiration. When lactate was applied in medium gassed with 100% N2, lactate induced
acidification was 12.6% faster than in medium gassed with 100% O2. Thus, CO2 produced on
the pathway transferring redox energy from substrates like glucose and lactate to ADP and
phosphate via oxidative phosphorylation, may support further lactate uptake. The findings of
this work suggest an auto regulation of lactate uptake via CO2 release in ventricular mouse
cardiomyocytes.

Der vorliegende Beitrag geht aus der Beobachtung hervor, dass die Begriffe „Unternehmensinteresse“, „Unternehmensziele“, „Unternehmenszweck“, „Gesellschaftsinteresse“, „Gesellschaftsziele“ und „Gesellschaftszweck“ in der Literatur häufig undifferenziert oder synonym verwendet werden. Die Frage, worauf bzw. wozu der Vorstand einer Aktiengesellschaft verpflichtet ist oder, anders ausgedrückt, welche Leitmaximen der Vorstand zu berücksichtigen hat, kann daher konzeptionell nicht klar beantwortet werden.
Ziel des Beitrages ist es, die genannten Begriffe eindeutig zu definieren und sie voneinander abzugrenzen. Dazu werden die folgenden beiden Forschungsfragen beantwortet:
1) Wie können das Unternehmensinteresse, die Unternehmensziele und der Unternehmenszweck voneinander abgrenzt werden?
2) Wie können das Unternehmensinteresse, die Unternehmensziele und der Unternehmenszweck vom Gesellschaftsinteresse, den Gesellschaftszielen und dem Gesellschaftszweck abgegrenzt werden?

Der Bericht beinhaltet die Punkte "Informationstechnik und digitale Bibliotheksdienste", "Online-Fachdatenbanken und CD-ROM-Netz", "Elektronische Hochschulschriften, Lernmaterialien und Fotos", "E-Journals und E-Books", "Literatur- und Sachmittel", "Literaturerwerbung/Bestand", "Bestandserschließung", "Benutzung/Information", "Schulungen", "Öffentlichkeitsarbeit/Ausstellungen" und "Personelle Änderungen" innerhalb der Universitätsbibliothek Kaiserslautern für das Jahr 2013.

Mechanical ventilation of patients with severe lung injury is an important clinical treatment to ensure proper lung oxygenation and to mitigate the extent of collapsed lung regions. While current imaging technologies such as Computed Tomography (CT) and chest X-ray allow for a thorough inspection of the thorax, they are limited to static pictures and exhibit several disadvantages, including exposure to ionizing radiation and high cost. Electrical Impedance Tomography (EIT) is a novel method to determine functional processes inside the thorax such as lung ventilation and cardiac activity. EIT reconstructs the internal electrical conductivity distribution within the thorax from voltage measurements on the body surface. Conductivity changes correlate with important clinical parameters such as lung volume and perfusion. Current EIT systems and algorithms use simplified or generalized thorax models to solve the reconstruction problem, which reduce image quality and anatomical significance. In this thesis, the development of a clinically relevant workflow to compute sophisticated three-dimensional thorax models from patient-specific CT data is described. The method allows medical experts to generate a multi-material segmentation in an interactive and fast way, while a volumetric mesh is computed automatically from the segmentation. The significantly improved image quality and anatomical precision of EIT images reconstructed with these 3D models is reported, and the impact on clinical applicability is discussed. In addition, three projects concerning quantitative CT (qCT) measurements and multi-modal 3D visualization are presented, which demonstrate the importance and productivity of interdisciplinary research groups including computer scientists and medical experts. The results presented in this thesis contribute significantly to clinical research efforts to pave the way towards improved patient-specific treatments of lung injury using EIT and qCT.