43 research outputs found
Entwicklung und Implementierung von tools zur Erforschung von Stresserleben
No full textIn dieser kumulativen Dissertation werden drei Artikel vorgestellt, die sich inhaltlich mit der Entstehung, der Messung und den Auswirkungen von Stress auf kognitive Prozesse befassen. Gemeinsamer Fokus liegt neben der genetischen Prädisposition, auf der subjektiven Wahrnehmung der Stressbelastung sowie auf der Erforschung der Auswirkungen von Stress. So wurden in der ersten Studie (Erstautor) neben der subjektiven Erhebung ein objektiver, physiologischer Parameter (Herzrate) zur Dokumentation von Stress in einer akuten Stresssituationen erhoben und des Weiteren untersucht, wie sich Stress auf die kognitiven Prozesse Merkfähigkeit, räumliche Orientierung und kognitive Flexibilität auswirken. Neu an der von mir gewählten Herangehensweise ist in dieser Studie der Einsatz von virtueller Realität zur Stressinduktion und zur Messung der kognitiven Prozesse. In der zweiten Studie (Erstautor) wurde ein Fragebogen (SAM) zur Messung von subjektivem Stresserleben ins Deutsche übersetzt, validiert, und es fand aufgrund der Ergebnisse eine kritische Diskussion des prominenten Stressmodels von Lazarus und Folkman (1984) statt. Die dritte Studie (Co-Autor) befasste sich mit der genetischen Prädisposition für Stressfolgeerkrankungen. Es wurde untersucht, ob die Akt2 Single Nuclear Polymorphismen (SNPs) mit ängstlichen und depressiven Persönlichkeitseigenschaften in Zusammenhang stehen.
In meine Promotion sollte neben der genetischen, psychophysiologischen und neuropsychologischen Bearbeitung der einzelnen Glieder der Stressreaktionskette eine innovative Methode, die Virtuelle Realität (VR), einfliessen
Automatisierung der Terminierungsanalyse von Probalistischen Programmen
No full textDeciding termination of computer programs is one of the most infamous challenges in computer science. In this thesis, we automate the termination analysis of a class of probabilistic programs, called Prob-solvable loops, through (super-)martingale based proof rules. We establish incomplete but sound algorithms for almost-sure termination, positive-almost-sure termination, and the negations thereof. We achieve this, by exploiting the structural restrictions of Prob-solvable loops. The restrictions let us effectively compute asymptotic bounds on polynomial expressions of program variables. These bounds are then used to decide the preconditions of the probabilistic termination proof rules, like the supermartingale condition. For certifying the negation of almost-sure termination, we generalize existing proof rules involving repulsing supermartingales, to handle unbounded polynomial variable updates of programs. This generalization applies to general probabilistic programs even beyond Prob-solvable loops. Moreover, we identify a subclass of probabilistic programs and introduce a sound and complete procedure deciding almost-sure termination of such programs. Our identified subclass strictly subsumes the class of so-called constant probability programs, the largest decidable subclass currently known. We combine our proposed algorithms for probabilistic termination analysis in our new tool Amber. Experimental results demonstrate that Amber can handle probabilistic programs that are out of reach for other state-of-the-art tools.Die Terminierung von Computerprogrammen zu entscheiden ist eines der ersten und berüchtigtsten Probleme der Informatik. In dieser Arbeit automatisieren wir die Terminierungsanalyse einer Klasse von probabilistischen Programmen, der Klasse sogenannter Prob-solvable loops, mithilfe von Beweisregeln basierend auf Supermartingalen. Wir konstruieren Algorithmen für almost-sure-termination, positive-almost-sure-termination, sowie für die Negationen der Konzepte. Für diesen Zweck nutzen wir strukturelle Eigenschaften von Prob-solvable loops. Die Eigenschaften ermöglichen uns asymptotische Schranken für polynomielle Ausdrücke über Programmvariablen automatisch zu berechnen. Diese Schranken werden dann benutzt, um die Bedingungen der probabilistischen Beweisregeln, wie zum Beispiel die Bedingung für Supermartingale, zu überprüfen. Um die Negation von almost-sure-termination festzustellen, verallgemeinern wir existierende Beweisregeln, die auf repulsiven Supermartingalen basieren. Dies ermöglicht uns unbeschränkte, polynomielle Updates von Programmvariablen zu unterstützen. Die verallgemeinerte Beweisregel ist für allgemeine probabilistische Programme verwendbar und nicht nur für Prob-solvable loops. Weiters, identifizieren wir eine Subklasse von probabilistischen Programmen, für die wir einen vollständigen und korrekten Algorithmus entwickeln, welcher almost-sure-termination für Programme der Subklasse entscheidet. Unsere identifizierte Subklasse ist strikt größer als die Klasse sogenannter constant-probability-programs, welches die größte derzeit bekannte Klasse ist, für die almost-sure-termination entscheidbar ist. Wir kombinieren die entwickelten Algorithmen für die probabilistische Terminierungsanalyse in unserem neuen Softwaretool Amber. Experimentelle Ergebnisse zeigen, dass Amber probabilistische Programme handhaben kann, die unerreichbar für andere state-of-the-art Tools sind
Automated analysis of probabilistic loops
No full textThis thesis addresses challenges and advancements in the automated analysis of probabilistic loops. It contributes to the theoretical foundations and computational techniques for analyzing the safety and liveness of probabilistic loops. A core contribution is the development of a fully automated method for computing higher moments of program variables for a large class of probabilistic loops. This method leverages linear recurrences with constant coefficients to model higher moments of loop variables and compute their exact closed-form expressions. Introducing the theory of moment-computable loops, we show that our approach is complete for a class of programs supporting branching statements, polynomial arithmetic, and both discrete and continuous probability distributions. For probabilistic systems with unknown model parameters, we introduce a novel technique for automatic sensitivity analysis with respect to these parameters. By representing unknown parameters with symbolic constants and modeling sensitivities using recurrences, we show that our technique is applicable even to loops that are not moment-computable. Furthermore, this thesis explores hardness bounds for computing the strongest polynomial invariant for classical polynomial loops, showing that this problem SKOLEM-hard. As an intermediary result of independent interest, we show that point-to-point reachability for polynomial dynamical systems is also SKOLEM-hard. Through the notion of moment invariant ideals, we extend these hardness results from classical to probabilistic program analysis. Despite the hardness results, we propose a method for computing polynomial invariants of bounded degree for (probabilistic) polynomial loops and a synthesis procedure to over-approximate polynomial loops with linearizable loops. Additionally, the thesis introduces POLAR, a tool implementing the developed techniques,demonstrating its capability to analyze benchmarks previously out of reach for state-of-the-art methods. Regarding termination analysis, we propose a novel approach based on asymptotic bounds for polynomial probabilistic loops, leading to the development of AMBER, the first tool to certify both probabilistic termination and non-termination
Kohelet und der materielle Reichtum. Koh 5,12–6,12 als eine Konkretisierung seines weisheitlichen Denkens
No full textThe book of Ecclesiastes as one of the few parts of the bible, which is in the very spotlight of modern forms of spirituality, is very likely to be misunderstood as a book promoting hedonism and irresponsibility – not only by common people, but also by theologians and exegetes. In contrary this essay tries to read Ecclesiastes regarding the cultural background of the accelerating hellenization of the Israelite world, which nevertheless appears to be quite a stable foundation. Thus, there is no understanding of difficult passages such as Ecclesiastes 5:12–6:12, which is one of the most important parts of this book as far as hermeneutics is concerned, if the traditional Israelite point of view is neglected. A closer look on these verses, which deal with the problematic phenomenon of material fortune, exemplifies that the author of Ecclesiastes is neither a cynic hedonist nor an indifferentstoic, but a wise man standing with both feet on the ground of traditional-biblical convictions. He uses the popular hellenistic philosophy as a tool not in order to create a new philosophy-based Weltanschauung, but to find new forms of legitimation of the old Israelite faith in times of a changing cultural world
Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs
No full textWe show that computing the strongest polynomial invariant for single-path
loops with polynomial assignments is at least as hard as the Skolem problem, a
famous problem whose decidability has been open for almost a century. While the
strongest polynomial invariants are computable for affine loops, for polynomial
loops the problem remained wide open. As an intermediate result of independent
interest, we prove that reachability for discrete polynomial dynamical systems
is Skolem-hard as well. Furthermore, we generalize the notion of invariant
ideals and introduce moment invariant ideals for probabilistic programs. With
this tool, we further show that the strongest polynomial moment invariant is
(i) uncomputable, for probabilistic loops with branching statements, and (ii)
Skolem-hard to compute for polynomial probabilistic loops without branching
statements. Finally, we identify a class of probabilistic loops for which the
strongest polynomial moment invariant is computable and provide an algorithm
for it.Comment: Published at POPL 202
Automated Sensitivity Analysis for Probabilistic Loops
No full textWe present an exact approach to analyze and quantify the sensitivity of
higher moments of probabilistic loops with symbolic parameters, polynomial
arithmetic and potentially uncountable state spaces. Our approach integrates
methods from symbolic computation, probability theory, and static analysis in
order to automatically capture sensitivity information about probabilistic
loops. Sensitivity information allows us to formally establish how value
distributions of probabilistic loop variables influence the functional behavior
of loops, which can in particular be helpful when choosing values of loop
variables in order to ensure efficient/expected computations. Our work uses
algebraic techniques to model higher moments of loop variables via linear
recurrence equations and introduce the notion of sensitivity recurrences. We
show that sensitivity recurrences precisely model loop sensitivities, even in
cases where the moments of loop variables do not satisfy a system of linear
recurrences. As such, we enlarge the class of probabilistic loops for which
sensitivity analysis was so far feasible. We demonstrate the success of our
approach while analyzing the sensitivities of probabilistic loops
Fragen des Christen: Bilanz einer religiösen Sendereihe des ORF
No full textIm Juni 1975 läutete das Telefon. Ernst Niesner, damals Leiterder Abteilung Kirche im Fernsehen, rief an, ob ich nicht Lust hätte, bei einer neuen Sendereihe mitzumachen. Man wüßte zwar noch nicht genau, wie sie ausschauen sollte, aber das Wichtigste wäre aufjeden Fall, daß man ganz auffeedbackausgehen wollte, auf Gespräch mit dem Zuschauer. Die Themen sollten aus der Zuschauerschar selbst kommen, und in der letzten Sendung wollte man sogar schon auf die Briefe der vorhergehenden Sendung eingehen. Aber alles andere würde sich ganz von selbst aus den Reaktionen und Erfahrungen ergeben. Diese Fünfminutensendung war also irgendwie eine Nachahmung von Pfarrer Sommemuers Hitsendung aus dem Bayerischen Fernsehen. (...) English The "Chruch and TV" Department ofth Austrian Radio and Television Network !ORF) has for about three years aired a programme entitled "Questions the Christian asks." This programme aims at pastoral contacts and care rather than evangelisation. The live minute transmission is on Saturday evenings after 10 o\u27clock, sandwiched between Sport and a Detective programme. The content is determined by viewers themselves, and pictures and illustrations are used with thesubjects treated. Its success seems to be considerable, and there are 1,000 personalletters a year, many phone calls, and also visits. The programme fills a gap in the unsuspected loneliness of modern man and his deep human sorrows which cannot be formulated or analysed when alone. The "home effects" of television, meeting man in his private and personal environment, helps to build up a semblance of partnership. The positive attitude of the programme and a certainhuman warmth of the speakers manages to break through the block built up against human relationships. Letter and phone are media which are on the one hand sufficiently anonymaus to Iet the loneliness remain, but, on the other hand, can build up a personal relationship. This programme demonstrates a new form of pastoral care which could provide openings for the Church. The author is one of the speakers in the series and at the same time parish priest in a small Tyrolean village.
Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs
No full textWe show that computing the strongest polynomial invariant for single-path loops with polynomial assignments is at least as hard as the Skolem problem, a famous problem whose decidability has been open for almost a century. While the strongest polynomial invariants are computable for affine loops, for polynomial loops the problem remained wide open. As an intermediate result of independent interest, we prove that reachability for discrete polynomial dynamical systems is Skolem-hard as well. Furthermore, we generalize the notion of invariant ideals and introduce moment invariant ideals for probabilistic programs. With this tool, we further show that the strongest polynomial moment invariant is (i) uncomputable, for probabilistic loops with branching statements, and (ii) Skolem-hard to compute for polynomial probabilistic loops without branching statements. Finally, we identify a class of probabilistic loops for which the strongest polynomial moment invariant is computable and provide an algorithm for it
This is the Moment for Probabilistic Loops - Artifact (Polar)
No full textArtifact acompanying the paper "This is the Moment for Probabilistic Loops".
Please download the zip file which contains a README.md file with instructions and a Docker image
