University of Kaiserslautern
KLUEDO Publication Server of University of Kaiserslautern-Landau (RPTU)Not a member yet
6017 research outputs found
Sort by
Ramsey Quantifiers in First-Order Logic: Complexity and Applications to Verification
Get PDFThe verification of software correctness is becoming increasingly important due to the widespread use of computers,
particularly in safety-critical environments.
Many complex systems (such as those involving numeric data types, recursion, or multithreading)
naturally exhibit an unbounded number of program states (a.k.a. configurations).
These are referred to as infinite-state systems and
their verification is an active research area with numerous unresolved problems.
A key focus in this field is the verification of safety and liveness properties.
While safety verification can be reduced to reachability via finite paths,
liveness verification involves reasoning about infinite executions, making it considerably more challenging.
Most approaches for checking liveness properties are devised for specific classes of systems.
We study so-called Ramsey quantifiers,
which state the existence of infinite cliques in the graph defined by a formula, in various first-order theories.
We show that over automatic structures, which is the class of first-order structures whose domain and relations are regular,
Ramsey quantifiers can be evaluated in logarithmic space.
For tree-regular relations we give a polynomial-time evaluation algorithm
if a deterministic bottom-up tree automaton is provided or if the relation is transitive.
We furthermore study Ramsey quantifiers in more specific theories.
Linear arithmetics over integers/reals are prominent theories featured in SMT solvers.
We show that the Ramsey quantifier can be eliminated from existential formulas in
linear arithmetic over the integers, reals, and their mixture in polynomial time.
This directly enables the use of highly optimized SMT solvers.
As an application, we provide a general framework for liveness verification across a wide range of infinite-state systems.
For example, we prove precise complexity results for recurrent reachability with generalized Büchi condition over (tree-)regular relations and linear liveness for succinct one-counter automata, reversal-bounded counter machines,
continuous vector addition systems with states, and
Parikh automata.
As a second major application, we identify the problem of checking whether a given formula is monadically decomposable,
i.e. equivalent to a Boolean combination of formulas, each depending only on a single free variable.
Monadic decompositions can, for example, be used in constraint databases, string analysis, and quantifier elimination.
We prove precise complexity results in the case of quantifier-free formulas in linear integer/real arithmetic.
We additionally explore a related problem: checking whether a relation on words (resp. trees) is (tree-)recognizable,
i.e. a finite union of Cartesian products of (tree-)regular languages
Die Umsetzung der sog. EU-Notfallverordnung (Verordnung EU 2022/2577) in Deutschland: Tatsächliche Beschleunigung für den Ausbau erneuerbarer Energien?
Get PDFDie Masterarbeit versucht die im Titel aufgeworfene Frage zu beantworten, nämlich, ob die EU-Notfallverordnung (Verordnung EU 2022/2577) den Ausbau der erneuerbaren Energien in Deutschland beschleunigt hat
Die Auswirkungen Generativer Künstlicher Intelligenz (KI) auf Führungsstrukturen in modernen Organisationen
Get PDFDie Masterarbeit untersucht, wie der Einsatz generativer Künstlicher Intelligenz (KI) – insbesondere Large Language Models wie ChatGPT – die Strukturen und Rollen in modernen Führungsprozessen verändert. Auf Basis einer systematischen Literaturrecherche werden klassische und moderne Führungstheorien (transaktional, transformational, situativ) analysiert und zu einem hybriden Führungsmodell weiterentwickelt. Die Arbeit beleuchtet Chancen, Risiken und Grenzen von KI-gestützter Führung, einschließlich ethischer, datenschutzrechtlicher und organisatorischer Aspekte. Im Fokus steht die Frage, wie Führungskräfte ihre Kompetenzen und Strategien anpassen müssen, um generative KI verantwortungsvoll und effektiv in Entscheidungsprozesse zu integrieren, ohne die menschliche Führungsverantwortung zu verlieren
Demokratiestabilisierung durch institutionellen Wandel? Eine makrosoziologische Betrachtung der Entwicklung politischer Unterstützung nach strukturellen und prozessualen Veränderungen im wiedervereinigten Deutschland.
Get PDFDie vorliegende kumulative Dissertation widmet sich der Frage nach der Persistenz demokratischer politischer Systeme in Zeiten zunehmender globaler Krisen und gesellschaftlicher Umbrüche. Die Arbeit verortet sich in der Tradition der politischen Kulturforschung und analysiert, wie strukturelle und prozessuale Veränderungen innerhalb eines politischen Systems die Einstellungen der Bürgerinnen und Bürger gegenüber der Demokratie langfristig beeinflussen. Die übergeordnete Forschungsfrage lautet, wie sich Demokratie befürwortende Einstellungen nach institutionellen Veränderungen in zeitlicher Perspektive entwickeln.
Als theoretischer Rahmen dient das Konzept der Politischen Unterstützung von David Easton, das zwischen langfristig stabilen Legitimitätsüberzeugungen (diffuse Unterstützung) und kurzfristig schwankenden, output-bezogenen Bewertungen (spezifische Unterstützung) differenziert. Die Arbeit untersucht, inwiefern die politische Sozialisation in unterschiedlichen politischen Systemen und die Erfahrung mit partizipativen institutionellen Mechanismen die Demokratieunterstützung, das Demokratieverständnis und die Demokratiezufriedenheit prägen.
Die Analysen basieren auf langfristig angelegten Umfragedaten in zwei quasi-experimentellen Settings. Zum einen dient die deutsche Wiedervereinigung als Kontext, um die Auswirkungen der politischen Sozialisation in der BRD und der DDR auf Demokratie befürwortende Einstellungen zu vergleichen. Zum anderen wird eine direkt-demokratische Abstimmung in Baden-Württemberg (Stuttgart 21) als quasi-experimentelles „Treatment“ herangezogen, um den Einfluss von Partizipationsprozessen auf die Demokratiezufriedenheit zu untersuchen.
Die drei in die Dissertation eingebrachten Studien leisten einen substanziellen Beitrag zur Schließung bestehender Forschungslücken. Die erste Studie befasst sich mit der Messung der Demokratieunterstützung und zeigt, dass die politische Sozialisation in der DDR auch nach der Wiedervereinigung zu einer geringeren Demokratieunterstützung führt, sich diese Unterschiede durch eine gemeinsame Sozialisation in der BRD jedoch aufheben. Die zweite Studie untersucht den bisher wenig beachteten Einfluss der Sozialisation auf das Demokratieverständnis und belegt, dass sich das Demokratieverständnis zwischen Ost- und Westdeutschland langfristig angleicht, wobei die Unterschiede in der normativen Bewertung der Demokratie allmählich abnehmen. Schließlich analysiert die dritte Studie den Effekt der Teilnahme an direkt-demokratischen Abstimmungen auf die politische Unterstützung und zeigt, dass die aktive Partizipation an einem solchen Prozess zu einem signifikanten Anstieg der Zufriedenheit mit der Demokratie bei den Teilnehmenden führt.
Zusammenfassend liefert die Arbeit empirische Evidenz dafür, welche Rolle institutionelle Strukturen und Prozesse für die Entwicklung einer demokratischen, unterstützenden Bürgerbasis spielen. Sie trägt somit zum Verständnis bei, wie Demokratien ihre Stabilität sichern und demokratische Resilienz aufgebaut werden kann
Human diseases and exposure to pesticides in developing countries: temporal spatial analysis, risk mitigation strategies and spatial decision support system
Get PDFIn developing countries, an increasing number of cases of chronic kidney disease (CKD) is observed, in which traditional risk factors for CKD can be ruled out. In such cases, the term chronic kidney disease of unknown etiology (CKDu) is used. A causal relationship between potential risk factors and the onset of the disease has not been clearly established, yet. However, agrochemicals are suspected to be associated with the disease. This dissertation aims to contribute to the reduction of exposure to the potential risk factor agrochemicals.
The first part of the work describes the characteristics of CKDu, the situation in developing countries, and their agricultural practices. Developing countries and their agricultural sectors are often marked by a lack of financial and infrastructural resources as well as comparatively low levels of education. The occurrence of CKDu has been documented in various regions around the world.
Based on this, the second part of the work adapts a research and development environment to local conditions, using the concept Living Lab. The Living Lab serves to develop, validate, and improve tailored risk mitigation strategies concerning agrochemical use. These strategies are introduced by various stakeholders involved in the Living Lab as potential solutions. Both, the Living Lab itself and the resulting risk mitigation measures are designed as low-cost approaches, for instance through the use of open-source software.
The third part of the dissertation describes and develops exemplary low-cost risk mitigation strategies from the fields of ecotoxicology and mathematical modeling. These serve as a base for further development of risk mitigation strategies within the research and development cycle of the Living Lab.
In the final part of the work, various mathematical methods are presented for the development of an adaptive decision support system. This system is capable of processing spatial, temporal, and fuzzy data to generate appropriate decision support related to the potential risk factor agrochemicals.In Entwicklungsländern ist eine zunehmende Anzahl von Fällen chronischer Niereninsuffizienz (CKD) zu beobachten, wobei traditionelle Risikofaktoren für CKD ausgeschlossen werden können. In solchen Fällen spricht man von chronischer Niereninsuffizienz unbekannter Herkunft (CKDu). Eine ursächliche Verbindung zwischen potenziellen Risikofaktoren und dem Auftreten der Krankheit konnte bislang nicht eindeutig nachgewiesen werden. Es besteht jedoch der Verdacht, dass Agrochemikalien mit der Krankheit in Zusammenhang stehen könnten. Die vorliegende Dissertation soll einen Beitrag zur Reduzierung der Exposition gegenüber dem potenziellen Risikofaktor Agrochemikalien leisten.
Im ersten Teil der Arbeit werden zunächst die Charakteristika von CKDu, die Situation in Entwicklungsländern sowie die dortige Landwirtschaft beschrieben. Entwicklungsländer und deren Agrarsektor sind häufig durch einen Mangel an finanziellen und infrastrukturellen Ressourcen sowie ein vergleichsweise niedriges Bildungsniveau gekennzeichnet. Das Auftreten von CKDu ist in verschiedenen Regionen weltweit dokumentiert.
Auf dieser Grundlage wird im zweiten Teil der Arbeit eine Forschungs- und Entwicklungsumgebung basierend auf dem Konzept des Living Lab an die beschriebenen Gegebenheiten angepasst. Das Living Lab dient der Entwicklung, Validierung und Verbesserung angepasster Risikominimierungsstrategien im Umgang mit Agrochemikalien. Diese Strategien werden von den verschiedenen beteiligten Akteuren im Rahmen des Living Lab als Lösungsvorschläge eingebracht. Sowohl das Living Lab als auch die entwickelten Maßnahmen zur Risikominimierung werden als kostengünstige Methoden konzipiert, beispielsweise durch den Einsatz von Open-Source-Software.
Im dritten Teil der Arbeit werden exemplarisch Low-Cost-Risikominimierungsstrategien aus den Bereichen Ökotoxikologie und mathematische Modellbildung beschrieben und entwickelt. Diese dienen als Grundlage für weiterentwickelbare Strategien innerhalb des Forschungs- und Entwicklungszyklus des Living Lab.
Im abschließenden Teil der Arbeit werden verschiedene mathematische Methoden vorgestellt, mit deren Hilfe ein adaptives Entscheidungsunterstützungssystem entwickelt werden kann. Dieses System ist in der Lage, räumliche, zeitliche und unscharfe Informationen zu verarbeiten und daraus fundierte Entscheidungshilfen im Bereich der Risikominimierung abzuleiten
Analysis of mitotic sister chromatid junctions in response to replication stress
Get PDFReplication stress has been extensively studied in the context of DNA synthesis defects and downstream consequences such as genomic instability and tumorigenesis. However, the specific mechanisms linking replication stress to mitotic errors, particularly the formation of persistent sister chromatid connections such as ultrafine anaphase bridges, remain insufficiently defined. Many proteins and regulatory pathways have been identified to manage these chromosome junctions throughout the cell cycle, either by preventing their formation or facilitating their resolution. While proteins such as BLM, PICH, and FANCD2 have been identified as ultrafine anaphase bridge-associated factors, their precise role in genome maintenance is not yet fully understood.
Considering the detrimental impact of mitotic errors on cell fate and their potential role in cancer development, it is essential to investigate further the roles of ultrafine anaphase bridge-associated proteins, their molecular interactions, and the mechanisms through which they preserve genomic integrity.
Using CRISPR/Cas9 technology, the generation of cell lines with controllable auxin-induced protein degradation provides a powerful tool for dissecting the functions of anaphase bridge-binding proteins, enabling precise investigation of their roles at specific cell cycle stages. Additionally, fluorescent tagging of target proteins facilitates protein detection and allows for real-time visualization.
This work provides a fundamental basis for the establishment of such degradation system-based cell lines via a modular cloning strategy as well as the successful generation of a cell line for the anaphase bridge-binding protein BLM for rapid and targeted research in specific contexts. Loss of functional BLM led to increased sister chromatid exchange, reduced proliferative capacity, and, especially under replication stress, a pronounced decline in colony-forming ability accompanied by elevated DNA damage, mitotic aberrations, and micronuclei formation. These observations highlight the critical role of BLM in preserving genomic integrity and sustaining cell viability, particularly under conditions that challenge the stability of the genome.
Additionally, it was observed, for the first time to our knowledge, that BLM’s association with ultrafine anaphase bridges during mitosis represents a function that is independent of its roles in other phases of the cell cycle. Using the AID system, this finding suggests that BLM operates through stage-specific mechanisms that are not necessarily interconnected. In particular, the exclusive role of BLM during mitosis is shown to be critical for attenuating the development of mitotic aberrations and anaphase bridges, thereby preventing deleterious consequences such as genomic instability.Replikationsstress ist im Zusammenhang mit DNA-Synthesedefekten und den sich daraus ergebenden Folgen wie genomische Instabilität und Tumorentstehung eingehend untersucht worden. Die spezifischen Mechanismen, die Replikationsstress mit mitotischen Fehlern verbinden, insbesondere die Bildung persistenter Schwesterchromatidenverbindungen wie ultrafeine Anaphase-Brücken, sind jedoch noch unzureichend definiert. Es wurden zahlreiche Proteine und Regulationswege identifiziert, die diese Chromosomenverbindungen während des Zellzyklus steuern, indem sie entweder ihre Bildung verhindern oder ihre Auflösung erleichtern. Während Proteine wie BLM, PICH und FANCD2 als ultrafeine Anaphase-Brücken-assoziierte Faktoren identifiziert wurden, ist ihre genaue Rolle bei der Erhaltung des Genoms noch nicht vollständig geklärt.
In Anbetracht der schädlichen Auswirkungen mitotischer Fehler auf das Zellschicksal und ihrer potenziellen Rolle bei der Krebsentstehung ist es von entscheidender Bedeutung, die Rolle der ultrafeinen Anaphase-Brücken-assoziierten Proteine, ihre molekularen Interaktionen und die Mechanismen, durch die sie die genomische Integrität bewahren, weiter zu untersuchen.
Mit Hilfe der CRISPR/Cas9-Technologie können Zelllinien mit kontrollierbarem Auxin-induziertem Proteinabbau generiert werden, was ein wirkungsvolles Mittel zur Untersuchung der Funktionen von Anaphase-Brückenbindungsproteinen darstellt und eine präzise Untersuchung ihrer Rolle in bestimmten Zellzyklusphasen ermöglicht. Darüber hinaus erleichtert die Fluoreszenzmarkierung der Zielproteine den Nachweis der Proteine und ermöglicht eine Visualisierung in Echtzeit.
Diese Arbeit liefert eine grundlegende Basis für die Etablierung solcher auf dem Auxin-induziertem Proteinabbau basierender Zelllinien durch eine modulare Klonierungsstrategie. Zudem wurde für die schnelle und gezielte Forschung in spezifischen Kontexten erfolgreich eine Zelllinie für das Anaphase-Brückenbindungsprotein BLM generiert. Der Verlust des funktionellen BLM führte zu einem erhöhten Austausch von Schwesterchromatiden, einer verringerten Proliferationsfähigkeit und, insbesondere unter Replikationsstress, zu einem deutlichen Rückgang der Fähigkeit zur Koloniebildung, begleitet von erhöhten DNA-Schäden, mitotischen Aberrationen und der Bildung von Mikronuklei. Diese Beobachtungen unterstreichen die entscheidende Rolle von BLM bei der Erhaltung der genomischen Integrität und der Lebensfähigkeit der Zellen, insbesondere unter Bedingungen, die die Stabilität des Genoms in Frage stellen.
Darüber hinaus wurde zum ersten Mal unseres Wissens nach festgestellt, dass die Assoziation von BLM mit ultrafeinen Anaphase-Brücken während der Mitose eine Funktion darstellt, die unabhängig von seiner Rolle in anderen Phasen des Zellzyklus ist. Unter Verwendung des AID-Systems deutet diese Erkenntnis darauf hin, dass BLM durch zellzyklusspezifische Mechanismen wirkt, die nicht unbedingt miteinander verbunden sind. Insbesondere die ausschließliche Rolle von BLM während der Mitose erweist sich als wesentlich für die Abschwächung der Entwicklung von mitotischen Aberrationen und Anaphase-Brücken, wodurch schädliche Folgen wie genomische Instabilität verhindert werden
Monitoring-Methoden zur Absicherung von KI-basierter Software innerhalb automatisierter Fahrfunktionen
Get PDFKünstliche Intelligenz (KI) ermöglicht das Lösen von komplexen Aufgaben, die nicht oder nur eingeschränkt manuell zu spezifizieren sind. Anstatt Software auf Basis konkreter Regeln zu programmieren, lernt die KI komplexe Zusammenhänge eigenständig aus einer Vielzahl von Daten. Ein bekanntes Anwendungsbeispiel aus der Industrie ist die Umgebungswahrnehmung beim automatisierten Fahren mithilfe von tiefen neuronalen Netzen. Die Vorteile des datengetriebenen Entwicklungsansatzes gehen jedoch im Kontext der funktionalen Sicherheit mit großen Herausforderungen einher. Bekannte Unzulänglichkeiten von KI, wie bspw. die mangelnde Interpretierbarkeit oder die mangelnde Repräsentation von Unsicherheiten, erschweren den Einsatz in sicherheitsrelevanten Systemen. Ein bedeutsamer Sicherheitsmechanismus stellt in diesem Zusammenhang die Überwachung von KI-basierter Software zur Laufzeit dar. Durch zusätzliches Monitoring können falsche Vorhersagen der KI erkannt werden, um Fail-Safe-Strategien und nachträgliche System-Verbesserungen zu unterstützen. In dieser Dissertation wird die Laufzeit-Überwachung von KI innerhalb automatisierter Fahrfunktionen unter Berücksichtigung etablierter Sicherheitsstandards im Automobilbau betrachtet. In diesem Zusammenhang wird ein generisches Monitor-Modell zur Überwachung unterschiedlicher KI-spezifischer Unzulänglichkeiten entwickelt. Hierzu werden heterogene Monitore zur Anomalie-Erkennung, Plausibilisierung, Erklärung, Eingangsrauschen-Erkennung und Unsicherheits-Berechnung in einem Metamodell kombiniert. Im Rahmen der experimentellen Untersuchung am Anwendungsfall der Verkehrszeichen-Erkennung wird eine zuverlässige Detektion von KI-bedingten Fehlern durch das Monitor-Modell demonstriert.Artificial Intelligence (AI) enables the solving of complex tasks, which cannot be specified manually or only to a limited extent. Instead of programming software on the basis of specific rules, the AI learns complex tasks independently from a variety of data. A well-known application example from the industry is the environmental perception in automated driving using deep neural networks. However, the advantages of the data-driven development approach are associated with major challenges in the context of functional safety. Known insufficiencies of AI, such as black-box characteristics or the lack of uncertainty representation, make it difficult to use in safety-relevant systems. An important safety mechanism in this context is the monitoring of AI-based software during runtime. Additional monitoring enables the detection of false AI predictions in order to support fail-safe strategies and subsequent system improvements. This doctoral thesis investigates the runtime monitoring of AI within automated driving functions taking into account established automotive safety standards. In this context, a generic monitor model is developed to observe different AI-specific insufficiencies. Therefore, heterogeneous monitors for anomaly detection, plausibility checks, explanation, input noise detection, and uncertainty estimation are combined in a metamodel. As part of the experimental evaluation on traffic sign recognition use case, a reliable detection of AI-related faults by the monitor model is demonstrated
Environmental Commitment at the Crossroads? Exploring the Dialectic of Risk Prevention and Climate Protection
Get PDFAmid escalating climate change and delayed political measures to prevent them, questions of how individuals negotiate the tension between collective climate protection and personal disaster preparedness have become increasingly urgent. This study explores these dynamics by examining the biography of ‘Lukas Sandner’, a sustainability activist whose trajectory reflects a shift from collective climate action to personal adaptation. Using a reconstructive biographical analysis based on a biographical narrative interview and the documentary method, the study reconstructs the interpretive frameworks and orientations that shape his actions and that situate him within this tension. The analysis shows that transformative learning was triggered by a disorienting event—particularly a severe heavy rainfall event—which redirected his focus from collective prevention efforts towards individual preparedness. His strategies include stockpiling, technical measures, and gardening understood as a hybrid practice linking ecological ideals with precautionary foresight. These shifts are dialectical, shaped by earlier experiences of concealment and reframing. The findings illustrate how personal trajectories intersect with broader social dynamics, showing how biographical experiences, structural conditions, and collective discourses converge to shape preparedness, highlighting the interplay between collective responsibility
and private resilience. The reconstruction of Sandner’s biography may provide clues to underlying societal trends toward individualised adaptation and risk prevention strategies in industrialised societies in response to growing disillusionment about the possibility of preventing climate change
Extraction and Characterization of TiO2 Pigments from Commercial Paints for Environmental Studies
Get PDFTiO2 nanoparticles are found as pigments in coatings and paints and are, therefore, released into the environment through runoff. To assess their environmental impact, comprehensive fate and ecotoxicity studies necessitate particles closely resembling those released into the environment. In response, we developed a method designed to isolate TiO2 particles from commercial paints. Using six contrasting paints alongside a pure TiO2 pigment, we evaluated two extraction methods in terms of recovery, purification rate, and preservation of both inorganic and organic particle coatings. The paints and extracts were characterized using cryogenic-TEM, ICP-OES, thermogravimetry, and infrared spectroscopy. In contrast to the alkaline-based extraction method, the extraction with acetic acid facilitated the retention of both inorganic and organic coatings and ensured good removal of organic polymers. Recovery rates exceeded 70% for all paints and extraction methods, yet the complete removal of SiO2, when present, was not achieved. CaCO3 removal was effective with both extraction methods. Our developed extraction method enables the isolation of TiO2-particles similar to those aged within paints. However, we recommend using silicate-free paints when SiO2 interference is of concern for the study design. Furthermore, this method could be interesting for pigment recycling, offering a gentler alternative to existing techniques which compromise particle coatings
Zukunftskompetenzen für OE-Berater - Erfolgsfaktoren eines Kompetenzprofils von morgen
Get PDFIn einer zunehmend unsicheren Zukunft müssen Organisationen ihre Wandlungsfähigkeit kontinuierlich demonstrieren, wobei die professionelle Organisationsentwicklung (OE) eine immer entscheidendere Rolle einnimmt. OE-Berater sehen sich daher mit der Herausforderung konfrontiert, der ansteigenden Komplexität mit aktuellen Kompetenzen zu begegnen. Die vorliegende theoretische Arbeit untersucht, auf welchen Zukunftskompetenzen und Erfolgsfaktoren ein Kompetenzprofil für OE-Berater basiert, das Zukunftsszenarien einbezieht. Auf Basis eines interdisziplinär ausgerichteten Kompetenzverständnisses wird ein aktuelles OE-Kompetenzprofil anhand von acht Megatrends einer kritischen Zukunftsbewertung unterzogen. Die gewonnenen Erkenntnisse werden abschließend in einem erweiterten, dreidimensionalen OE-Berater Zukunftskompetenzmodell dargestellt, das aus Konstanten, den Metakompetenzen besteht. Diese umfassen "Future Fitness", "Gleichwürdigkeit", "Komplexitätsmanagement", "Kreativität", "Reflexion" und "Resilienz". Das Modell wird zudem durch zwei Variablen ergänzt, die individuellen Kompetenzen des OE-Beraters und die Prozess- bzw. Fachkompetenz. Das OE-Berater Zukunftskompetenzmodell bietet durch seine mehrdimensionale Sichtweise eine neue, theoriegeleitete Perspektive auf aktuell und zukünftig relevante Kompetenzen und Erfolgsfaktoren. Darüber hinaus kann das Modell auch für weitere Berufsgruppen adaptiert werden