Refine
Year of publication
Document Type
- Preprint (759)
- Article (402)
- Working Paper (119)
- Doctoral Thesis (93)
- Diploma Thesis (47)
- Conference Proceeding (41)
- Book (37)
- Bachelor Thesis (36)
- diplomthesis (28)
- Report (25)
Has Fulltext
- yes (1619)
Is part of the Bibliography
- no (1619)
Keywords
Institute
- Informatik (1619) (remove)
Towards correctness of program transformations through unification and critical pair computation
(2010)
Correctness of program transformations in extended lambda-calculi with a contextual semantics is usually based on reasoning about the operational semantics which is a rewrite semantics. A successful approach is the combination of a context lemma with the computation of overlaps between program transformations and the reduction rules, which results in so-called complete sets of diagrams. The method is similar to the computation of critical pairs for the completion of term rewriting systems. We explore cases where the computation of these overlaps can be done in a first order way by variants of critical pair computation that use unification algorithms. As a case study of an application we describe a finitary and decidable unification algorithm for the combination of the equational theory of left-commutativity modelling multi-sets, context variables and many-sorted unification. Sets of equations are restricted to be almost linear, i.e. every variable and context variable occurs at most once, where we allow one exception: variables of a sort without ground terms may occur several times. Every context variable must have an argument-sort in the free part of the signature. We also extend the unification algorithm by the treatment of binding-chains in let- and letrec-environments and by context-classes. This results in a unification algorithm that can be applied to all overlaps of normal-order reductions and transformations in an extended lambda calculus with letrec that we use as a case study.
This paper shows the equivalence of applicative similarity and contextual approximation, and hence also of bisimilarity and contextual equivalence, in the deterministic call-by-need lambda calculus with letrec. Bisimilarity simplifies equivalence proofs in the calculus and opens a way for more convenient correctness proofs for program transformations. Although this property may be a natural one to expect, to the best of our knowledge, this paper is the first one providing a proof. The proof technique is to transfer the contextual approximation into Abramsky's lazy lambda calculus by a fully abstract and surjective translation. This also shows that the natural embedding of Abramsky's lazy lambda calculus into the call-by-need lambda calculus with letrec is an isomorphism between the respective term-models.We show that the equivalence property proven in this paper transfers to a call-by-need letrec calculus developed by Ariola and Felleisen.
This note shows that in non-deterministic extended lambda calculi with letrec, the tool of applicative (bi)simulation is in general not usable for contextual equivalence, by giving a counterexample adapted from data flow analysis. It also shown that there is a flaw in a lemma and a theorem concerning finite simulation in a conference paper by the first two authors.
A logical framework consisting of a polymorphic call-by-value functional language and a first-order logic on the values is presented, which is a reconstruction of the logic of the verification system VeriFun. The reconstruction uses contextual semantics to define the logical value of equations. It equates undefinedness and non-termination, which is a standard semantical approach. The main results of this paper are: Meta-theorems about the globality of several classes of theorems in the logic, and proofs of global correctness of transformations and deduction rules. The deduction rules of VeriFun are globally correct if rules depending on termination are appropriately formulated. The reconstruction also gives hints on generalizations of the VeriFun framework: reasoning on nonterminating expressions and functions, mutual recursive functions and abstractions in the data values, and formulas with arbitrary quantifier prefix could be allowed.
Zur genomweiten Genexpressionsanalyse werden Microarray-Experimente verwendet. Ziel dieser Arbeit ist es, Methoden zur Präprozessierung von Microarrays der Firma Affymetrix zu evaluieren und die VSN-Methode für Experimente mit weniger als 1000 Zellen zu verbessern. Bei dieser Technologie wird die Expression jedes Gens durch mehrere Probessets gemessen. Jedes Probeset besteht aus einem Perfect-Match (PM) und einem dazugehörigen Mismatch (MM). Der Expressionswert pro Gen wird durch ein vierstufiges Verfahren aus den einzelnen Probe-Werten berechnet: Hintergrundkorrektur, Normalisierung, PM-Adjustierung und Aggregation. Für jeden dieser Schritte existieren mehrere Algorithmen. Dazu dienten die im affy-Paket des Bioconductor implementierten Methoden MAS5, RMA, VSN und die Methode sRMA von Cope et al. [Cope et al., 2006] in Kombination mit der Methode VSN von Huber et al. [Huber et al., 2002]. Den ersten Teil dieser Arbeit bildet die Reanalyse der Datensätze von Küppers et al. [Küppers et al., 2003] und Piccaluga et al. [Piccaluga et al., 2007] mit der VSN-Methode. Dabei konnte gezeigt werden, dass die VSN-Methode gegenüber Klein et al. [Klein et al., 2001] Vorteile zeigt. Bei beiden Datensätzen wurden zusätzliche Gene gefunden, die für die Pathogenese der jeweiligen Tumorarten wichtig sein können. Einige der zusätzlich gefunden Gene wurden durch andere wissenschaftliche Arbeiten bestätigt. Die Gene, die bisher in keinem Zusammenhang mit der untersuchten Tumorart stehen, sind eine Möglichkeit für die weitere Forschung. Vor allem der Zytokine/Zytokine Signalweg wurde bei beiden Reanalysen als überrepräsentiert erkannt. Da für einige Microarray-Experimente die Anzahl der Zellen und damit die Menge an mRNA nur begrenzt zur Verfügung stehen, müssen die Laborarbeit und die statistischen Analysen angepasst werden. Hierzu werden fünf Methoden für die Präprozessierung untersucht, um zu evaluieren, welche Methode geeignet ist, derartige Expressionsdaten zu verrechnen. Auf Basis eines Testdatensatzes der bereits zur Etablierung des Laborprozesses diente werden Expressionswerte durch empirische Verteilung, Gammaverteilung und ein linear gemischtes Modell simuliert. Die Simulation lässt sich in vier Schritte einteilen: Wahl der Verteilung, Simulation der Expressionsmatrix, Simulation der differentiellen Expression, Sortierung der Probes innerhalb des Probesets. Anschließend werden die fünf Präprozessierungsmethoden mit diesen simulierten Expressionsdaten auf ihre Sensitivität und Spezifität untersucht. Während sich bei den empirisch und gammaverteilt simulierten Expressionsdaten kein eindeutiges Ergebnis abzeichnet, hat sVSN bei den Daten aus dem linear gemischten Modell die größte Sensitivität und die größte Spezifität. Der in dieser Arbeit entwickelte sVSN-Algorithmus wurde zum ersten Mal angewendet und bewertet. Abschließend wird ein Teildatensatz von Brune et al. verwendet und hinsichtlich der fünf Präprozessierungsmethoden untersucht. Die Ergebnisse der sVSN-Methode wird im Detail weiter verfolgt. Die zusätzlich gefunden Gene können durch bereits veröffentlichte Arbeiten bestätigt werden. Letztendlich zeigt sich, dass neuere statistische Methoden (wie das im Rahmen dieser Arbeit entwickelte sVSN) bei der Analyse von Affymetrix Microarrays einen Vorteil bringen. Die sVSN und sRMA Methoden zeigen Vorteile, da die Probes nach der Normalisierung gewichtet werden, bevor diese aggregiert werden. Die MAS5-Methode schneidet am schlechtesten ab und sollte bei geringen Zellmengen nicht eingesetzt werden. Für die Analyse mit geringer Menge an mRNA müssen weitere Untersuchungen vorgenommen werden, um eine geeignete statistische Methode für die Analyse der Expressionsdaten zu finden.
Ambiguity and communication
(2009)
The ambiguity of a nondeterministic finite automaton (NFA) N for input size n is the maximal number of accepting computations of N for an input of size n. For all k, r 2 N we construct languages Lr,k which can be recognized by NFA's with size k poly(r) and ambiguity O(nk), but Lr,k has only NFA's with exponential size, if ambiguity o(nk) is required. In particular, a hierarchy for polynomial ambiguity is obtained, solving a long standing open problem (Ravikumar and Ibarra, 1989, Leung, 1998).
Bayessche Methoden zur Schätzung von Stammbäumen mit Verzweigungszeitpunkten aus molekularen Daten
(2009)
Ein großes Ziel der Evolutionsbiologie ist es, die Stammesgeschichte der Arten zu rekonstruieren. Historisch verwendeten Systematiker hierfür morphologische und anatomische Merkmale. Mit dem stetigen Zuwachs an verfügbaren Sequenzdaten werden heute verstärkt Methoden entwickelt und eingesetzt, welche die Rekonstruktion auf Basis von molekularen Daten ermöglichen. Im Fokus der aktuellen Forschung steht die Anwendung und Weiterentwicklung Bayesscher Methoden. Diese Methoden besitzen große Popularität, da sie in Verbindung mit Markov-Ketten-Monte-Carlo-Verfahren eingesetzt werden können, um einen Stammbaum zu vorgegebenen Spezies zu schätzen und dessen Variabilität zu bestimmen. Im Rahmen dieser Dissertation wurde die erweiterbare Software TreeTime entwickelt. TreeTime bietet Schnittstellen für die Einbindung von molekularen Evolutions- und Ratenänderungsmodellen und stellt neu entwickelte Methoden bereit, um Stammbäume mit Verzweigungszeitpunkten zu rekonstruieren. In TreeTime werden die molekularen Daten und die zeitlichen Informationen, wie z.B. Fossilfunde, in einem Bayes-Verfahren simultan berücksichtigt, um die Zeitpunkte der Artaufspaltungen genauer zu datieren. Für die Anwendung Bayesscher Methoden in der Rekonstruktion von Stammbäumen wird ein stochastisches Modell benötigt, das die Evolution der molekularen Sequenzen entlang den Kanten eines Stammbaums beschreibt. Der Mutationsprozess der Sequenzen wird durch ein molekulares Evolutionsmodell definiert. Die Verwendung der klassischen molekularen Evolutionsmodelle impliziert die Annahme einer konstanten Evolutionsgeschwindigkeit der Sequenzen im Stammbaum. Diese Annahme wird als Hypothese der molekularen Uhr bezeichnet und bildet die Grundlage zum Schätzen der Verzweigungszeiten des Stammbaums. Der Verzweigungszeitpunkt, an dem sich zwei Spezies im Stammbaum aufspalten, spiegelt sich in der Ähnlichkeit der zugehörigen molekularen Sequenzen. Je älter dieser Verzweigungszeitpunkt ist, desto größer ist die Anzahl der unterschiedlichen Positionen in den Sequenzen. Häufig ist jedoch die Annahme der molekularen Uhr verletzt, so dass in gewissen Teilbereichen eines Stammbaums eine erhöhte Evolutionsgeschwindigkeit nachweisbar ist. Falls die Verletzung konstanter Evolutionsgeschwindigkeiten nicht ausgeschlossen werden kann, sollten schwankende Mutationsraten in der Modellierung explizit berücksichtigt werden. Hierfür wurden verschiedene Ratenänderungsmodelle vorgeschlagen. Bisher sind nur wenige dieser Ratenänderungsmodelle in Softwarepaketen verfügbar und ihre Eigenschaften sind nicht ausreichend erforscht. Das Ziel dieser Arbeit ist die Entwicklung und Bereitstellung von Bayesschen Modellen und Methoden zum Schätzen von Stammbäumen mit Verzweigungszeitpunkten. Die Methoden sollten auch bei unterschiedlichen Evolutionsgeschwindigkeiten im Stammbaum anwendbar sein. Vorgestellt wird ein neues Ratenänderungsmodell, eine neue Möglichkeit der Angabe von flexiblen Beschränkungen für die Topologie des Stammbaums sowie die Nutzung dieser Beschränkungen für die zeitliche Kalibrierung. Das neue Raten Änderungsmodell sowie die topologischen und zeitlichen Beschränkungen werden in einen modularen Softwareentwurf eingebettet. Durch den erweiterbaren Entwurf können bestehende und zukünftige molekulare Evolutionsmodelle und Ratenänderungsmodelle in die Software eingebunden und verwendet werden. Die vorgestellten Modelle und Methoden werden gemäß dem Softwareentwurf in das neu entwickelte Programm TreeTime aufgenommen und effzient implementiert. Zusätzlich werden bereits vorhandene Modelle programmiert und eingebunden, die nicht in anderen Softwarepaketen verfügbar sind. Des Weiteren wird eine neue Methode entwickelt und angewendet, um die Passgenauigkeit eines Modells für die Apriori-Verteilung auf der Menge der Baumtopologien zu beurteilen. Diese Methode wird zur Auswahl geeigneter Modelle benutzt, indem eine Auswertung der beobachteten Baumtopologien der Datenbank TreeBASE durchgeführt wird. Anschließend wird die Software TreeTime in einer Simulationsstudie eingesetzt, um die Eigenschaften der implementierten Ratenänderungsmodelle zu vergleichen. Die Software wird für die Rekonstruktion des Stammbaums zu 38 Spezies aus der Familie der Eidechsen (Lacertidae) verwendet. Da die zugehörigen molekularen Daten von der Hypothese der molekularen Uhr abweichen, werden unterschiedliche Ratenänderungsmodelle bei der Rekonstruktion verwendet und abschließend bewertet. ........
Gegenstand dieser Arbeit war die Analyse der Komplexität von Kosten- und Erlösrechnungssystemen und ihrer Auswirkung auf die Auswahl geeigneter Instrumente für die EDV-gestützte Realisierung dieser Systeme, wobei insbesondere auf die bisherigen Ansätze der Datenbank- und Wissensuntersrutzung der Kosten- und Erlösrechnung eingegangen werden sollte. Das zweite Kapitel befaßt sich mit einer Analyse der Komplexität der in Deutschland am weitesten verbreiteten Kosten- und Erlösrechnungssysteme. Die Untersuchung der grundlegenden Gestaltungsmerkmale von Kosten- und Erlösrechnungssystemen auf ihre Komplexitätsrelevanz zeigte, daß einige Merkmale die Komplexität sehr stark beeinflussen, andere dagegen kaum, darunter auch in der betriebswirtschaftlichen Diskussion so wesentliche wie der verwendete Kostenbegriff. Den größten Einfluß auf die Komplexität von Kosten- und Erlösrechnungssystemen besitzen die Kosten- und Erlösstrukturierung sowie die Verarbeitungsarten, -methoden und -inhalte. Ein Vergleich der Grenzplankostenrechnung nach Kn.GER und FLAUT, stellvertretend Im überwiegend zweckmonistische Kostenrechnungssysteme, und der Einzelkostenrechnung nach RIEBEL als zweckpluralistischem Kosten- und Erlösrechnungssystem bezüglich der komplexitätsrelevanten Merkmale ergab eindeutige Unterschiede zwischen diesen Systemen. Während die Grenzplankostenrechnung polynomiale Platz- und Funktionskomplexitäten niedriger Grade (überwiegend quadratisch und nur im Rahmen der innerbetrieblichen Leistungsverrechnung kubisch) aufweist, treten in der Einzelkostenrechnung an mehreren entscheidenden Stellen exponentielle Komplexitäten auf. Die Analyse der Komplexität dieser beiden Kosten- und Erlösrechnungssystemen zeigt einen eindeutigen Zusammenhang zwischen vielseitiger Auswertbarkeit und der Komplexität eines Systems auf, der bei einer Beurteilung von Kosten- und Erlösrechnungssystemen berücksichtigt werden muß. Für die Gestaltung von Kosten- und Erlösrechnungssystemen bedeutet dies eine grundsätzliche Wahlmöglichkeit zwischen Systemen begrenzter Auswertbarkeit und niedriger Komplexität sowie Systemen mit größerer Auswertungsvielfalt, aber deutlich höherer Komplexität. Die Komplexität von Kosten- und Erlösrechnungssystemen ist jedoch nicht als eine Folge der Auswahl eines Rechnungssystems zu betrachten, sondern resultiert letztlich aus der Komplexität einer Unternehmung und ihrer Umwelt, die unterschiedlich detailliert abgebildet werden können. Da diese Komplexitäten in Zukunft eher noch zunehmen werden, ist grundSätzlich mit einem Trend zu universelleren und komplexeren Systemen zu rechnen. Die Erweiterung der Grenzplankostenrechnung hin zu größerer Komplexität sowie die Entwicklung neuerer Ansätze wie der Prozeßkostenrechnung bestätigen beide diesen Trend. Für die weitere Untersuchung wird vorausgesetzt, daß die Grenzplankostenrechnung und die Einzelkostenrechnung die entgegengesetzten Enden eines Komplexitätsspektrums von Kosten- und Erlösrechnungssystemen bilden und daher auch das Spektrum der Anforderungen an die Instrumente zu ihrer EDV-Implementierung begrenzen. Unter einer Anzahl von neueren Entwicklungen in der EDV wurden daher zwei Konzepte ausgewählt, die zur Behandlung verschiedener Aspekte der Komplexität geeignet sind: Datenbanksysteme zur Behandlung der Platzkomplexität und Wissenssysteme zur Behandlung der Funktionskomplexität. Im folgenden werden die Erfahrungen, die bei der Realisierung von Datenbank- und Wissenssystemen für die Kosten- und Erlösrechnung gemacht wurden, unter dem Gesichtspunkt der Komplexität von Kosten- und Erlösrechnungssystemen bewertet. Bei der Betrachtung von Datenbanksystemen ist zu berücksichtigen, daß sich im Laufe der Zeit zwei unterschiedliche Anwendungstypen herauskristallisiert haben: konventionelle Datenbankanwendungen, die den herkömmlichen Paradigmen von Datenbanksystemen entsprechen, und neuere Datenbankanwendungen, die z.T. wesentlich höhere Anforderungen stellen und so die Entwicklung neuer Datenbanksysteme erforderlich machten. Beide Systeme der Kosten- und Erlösrechnung eignen sich grundSätzlich als Datenbankanwendungen, d.h. sie rechtfertigen den Einsatz von Datenbanksystemen zur Verwaltung ihrer Datenmengen. Während die Grenzplankostenrechnung aber den konventionellen Datenbankanwendungen zuzurechnen ist, weist die Einzelkostenrechnung bereits wesentliche Merkmale neuerer Datenbankanwendungen auf. Im Gegensatz zu Datenbanksystemen sind die Anforderungen an Wissenssysteme und ihre Eigenschaften sehr unpräzise, z.T. sogar widersprüchlich formuliert. Auf der Basis der gängigen Eigenschaftskataloge erscheint die Kosten- und Erlösrechnung nicht als typische Wissenssystemanwendung. Trotzdem wurden bereits mehrere Wissenssysteme für Kosten- und Erlösrechnungsprobleme (Abweichungsanalyse, Betriebsergebnisanalyse, Bestimmung von Preisuntergrenzen, konstruktionsbegleitende Kalkulation und Teilprobleme der Prozeßkostenrechnung) realisiert, von denen jedes einige der Eignungskriterien für Wissenssystemanwendungen erfüllt. Die behandelten Beispiele für Wissenssysteme im Rahmen der Kosten- und Erlösrechnung basieren überwiegend auf der Grenzplankostenrechnung. Es ist daher anzunehmen, daß die Einzelkostenrechnung auf Grund ihrer höheren Komplexität weitere Anwendungsprobleme für Wissenssysteme enthält. Insgesamt sind jedoch die Unterschiede zwischen der Grenzplankostenrechnung und der Einzelkostenrechnung im Hinblick auf den Einsatz von Wissenssystemen wesentlich weniger ausgeprägt als dies für den Einsatz von Datenbanksystemen der Fall war. Nachdem beide Systeme der Kosten- und Erlösrechnung sowohl als Datenbankanwendungen geeignet sind als auch Anwendungsprobleme für Wissenssysteme aufweisen, ist auch die Verbindung von Wissenssystemen und Datenbanksystemen in Betracht zu ziehen. Daher wurde im Anschluß die jeweiligen Vor- und Nachteile von Datenbank- und Wissenssysteme gegenübergestellt. Die Vorteile von Datenbanksystemen liegen auf den maschinennäheren Ebenen, auf denen die Vorkehrungen für Datenschutz, Datensicherung, reibungslosen Mehrbenutzerbetrieb sowie die effiziente Ausführung der Operationen geschaffen werden. Die Vorteile von Wissenssystemen liegen in der größeren Mächtigkeit der Problemlösungskomponente, der Wissenserweiterungskomponente und der Erklärungskomponente. Ein neueres Beispiel für eine Zusammenarbeit von Datenbank- und Wissenssystemen ist die Auswertung eines speziell für derartige Zwecke angelegten Data Warehouse durch das Data Mining sowie andere Analysesysteme. Ein Data Warehouse stimmt in wesentlichen Merkmalen mit der Grundrechnung der Einzelkostenrechnung überein und zeigt, daß eine Grundrechnung auf der Basis heutiger EDV -Systeme realisierbar ist. Zur Auswertung einer Datenbank dieser Größe sind spezielle Analysesysteme notwendig. Für standardisierte Auswertungen eines Data Warehouse wurden OLAP-Systeme entwickelt, deren Operationen Verallgemeinerungen mehrdimensionaler Deckungsbeitragsrechnungen sind. Bei nicht standardisierbaren Auswertungen empfiehlt sich dagegen der Einsatz von Wissenssystemen, für den das Data Mining ein Beispiel liefert. Diese Kombination von Datenbanksystem, konventionellen und Kl-Auswertungen erscheint für eine Verwendung in der Kosten- und Erlösrechnung bestens geeignet. Das vierte Kapitel befaßt sich mit Ansätzen zur Strukturierung von Daten- und Wissensbasen, die bei Datenbanksystemen als Datenmodelle, bei Wissenssystemen als Wissensrepräsentationstechniken bezeichnet werden. Dabei wurde der Unterteilung des dritten Kapitels gefolgt und zwischen konventionellen und neueren Datenmodellen sowie Wissensrepräsentationstechniken unterschieden. Die Betrachtung des Relationenmodells als Vertreters der konventionellen Datenmodelle ergab, daß es für die Grenzplankostenrechnung völlig ausreicht. Die Erfahrungen mit der Realisierung einer Grundrechnung auf der Basis des Relationenmodells haben dagegen gezeigt, daß seine syntaktischen und semantischen Mängel zu weitgehenden Vereinfachungen beim Schemaentwurf zwingen, die wiederum die Operationen der Auswertungsrechnungen unnötig komplizieren. Aus der Vielzahl semantischer und objektorientierter Datenmodelle, die für neuere Datenbankanwendungen entwickelt wurden, hat sich trotz Unterschieden in Details eine Anzahl von Konzepten herauskristallisiert, die den meisten dieser DatenmodelIe gemeinsam sind. Mit Hilfe dieser Konzepte sind die Probleme, die bei der Verwendung des Relationenmodelis auftraten, vermeidbar. Im Grunde sind daher fast alle semantischen und objektorientierten Entwurfsmodelle zur ModelIierung einer Grundrechnung geeignet. Wichtig ist jedoch,daß die Grundrechnung auch mit einem Datenbanksystem realisiert wird, dem eines dieser Datenmodelle zugrunde liegt, da bei einer Transformation auf ein relationales Datenmodell wesentliche Entwurfsüberlegungen - und damit der größte Teil des Vorteils,den semantische und objektorientierte Entwurfsmodelle bieten -, verloren gehen. Zur Realisierung einer Grundrechnung erscheinen objektrelationale Datenbanksysteme am besten geeignet, da sie einerseits objektorientierte Konzepte mit mächtigen und komfortablen Anfragesprachen verbinden und andererseits aufwärtskompatibel zu den weitverbreiteten relationalen Datenbanksystemen sind. Da sich die objektorientierten Datenmodelle als für die Modellierung einer Grundrechnung geeignet erwiesen haben, wurden unter dem Gesichtspunkt der Verbindung von Datenbank- und Wissenssystemen nur objektorientierte Wissensrepräsentationstechniken in Betracht gezogen. Zwischen semantischen und objektorientierten Datenmodellen einerseits und objektorientierten Wissensrepräsentationstechniken, vor allem semantischen Netzen und Frames, andererseits bestehen weitgehende Übereinstimmungen. Daher können z.B. framebasierte Wissenssysteme direkt auf objektorientierten Datenbanksystemen realisiert werden. Inzwischen werden aber auch objektorientierte Programmiersprachen wie C++ oder Smalltalk zur Implementierung von Wissenssystemen verwendet, von denen die objektorientierte Sprache C++ am geeignetsten erscheint, da die meisten objektorientierten und objektrelationalen Datenbanksysteme eine C++-Schnittstelle aufweisen. Abschließend ist daher festzustellen, daß das Paradigma der Objektorientierung, das in Entwurfssprachen, Datenmodellen, Wissensrepräsentationstechniken und Programmiersprachen wesentliche Einflüsse ausgeübt hat, für die Realisierung der datenbankgestützten Grundrechnung eines zweckpluralistischen Kosten- und Erlösrechnungssystems wie der Einzelkostenrechnung sowie darauf aufbauender Auswertungsrechnungen, die z.T. als Wissenssysteme realisiert werden, wesentliche Vorteile besitzt. Über die adäquatere ModelIierung der Strukturen hinaus entsteht durch den Einsatz objektorientierter Techniken zum Entwurf und zur Implementierung aller System teile ein möglichst homogenes System, das nicht zusätzlich zu der inhärenten Komplexität noch weitere Probleme durch ungeeignete Darstellungskonzepte oder schlechte Abstimmung schafft.
We provide the first non-trivial result on dynamic breadth-first search (BFS) in external-memory: For general sparse undirected graphs of initially $n$ nodes and O(n) edges and monotone update sequences of either $\Theta(n)$ edge insertions or $\Theta(n)$ edge deletions, we prove an amortized high-probability bound of $O(n/B^{2/3}+\sort(n)\cdot \log B)$ I/Os per update. In contrast, the currently best approach for static BFS on sparse undirected graphs requires $\Omega(n/B^{1/2}+\sort(n))$ I/Os. 1998 ACM Subject Classification: F.2.2. Key words and phrases: External Memory, Dynamic Graph Algorithms, BFS, Randomization.
Algorithms and data structures constitute the theoretical foundations of computer science and are an integral part of any classical computer science curriculum. Due to their high level of abstraction, the understanding of algorithms is of crucial concern to the vast majority of novice students. To facilitate the understanding and teaching of algorithms, a new research field termed "algorithm visualisation" evolved in the early 1980's. This field is concerned with innovating techniques and concepts for the development of effective algorithm visualisations for teaching, study, and research purposes. Due to the large number of requirements that high-quality algorithm visualisations need to meet, developing and deploying effective algorithm visualisations from scratch is often deemed to be an arduous, time-consuming task, which necessitates high-level skills in didactics, design, programming and evaluation. A substantial part of this thesis is devoted to the problems and solutions related to the automation of three-dimensional visual simulation of algorithms. The scientific contribution of the research presented in this work lies in addressing three concerns: - Identifying and investigating the issues related to the full automation of visual simulations. - Developing an automation-based approach to minimising the effort required for creating effective visual simulations. - Designing and implementing a rich environment for the visualisation of arbitrary algorithms and data structures in 3D. The presented research in this thesis is of considerable interest to (1) researchers anxious to facilitate the development process of algorithm visualisations, (2) educators concerned with adopting algorithm visualisations as a teaching aid and (3) students interested in developing their own algorithm animations.
Various concurrency primitives had been added to functional programming languages in different ways. In Haskell such a primitive is a MVar, joins are described in JoCaml and AliceML uses futures to provide a concurrent behaviour. Despite these concurrency libraries seem to behave well, their equivalence between each other has not been proven yet. An expressive formal system is needed. In their paper "On proving the equivalence of concurrency primitives", Jan Schwinghammer, David Sabel, Joachim Niehren, and Manfred Schmidt-Schauß define a universal calculus for concurrency primitives known as the typed lambda calculus with futures. There, equivalence of processes had been proved. An encoding of simple one-place buffers had been worked out. This bachelor’s thesis is about encoding more complex concurrency abstractions in the lambda calculus with futures and proving correctness of its operational semantics. Given the new abstractions, we will discuss program equivalence between them. Finally, we present a library written in Haskell that exposes futures and our concurrency abstractions as a proof of concept.
This paper gives a brief overview of computation models for data stream processing, and it introduces a new model for multi-pass processing of multiple streams, the so-called mp2s-automata. Two algorithms for solving the set disjointness problem with these automata are presented. The main technical contribution of this paper is the proof of a lower bound on the size of memory and the number of heads that are required for solving the set disjointness problem with mp2s-automata.
Iterative arrays (IAs) are a, parallel computational model with a sequential processing of the input. They are one-dimensional arrays of interacting identical deterministic finite automata. In this note, realtime-lAs with sublinear space bounds are used to accept formal languages. The existence of a proper hierarchy of space complexity classes between logarithmic anel linear space bounds is proved. Furthermore, an optimal spacc lower bound for non-regular language recognition is shown. Key words: Iterative arrays, cellular automata, space bounded computations, decidability questions, formal languages, theory of computation
It is shown that between one-turn pushdown automata (1-turn PDAs) and deterministic finite automata (DFAs) there will be savings concerning the size of description not bounded by any recursive function, so-called non-recursive tradeoffs. Considering the number of turns of the stack height as a consumable resource of PDAs, we can show the existence of non-recursive trade-offs between PDAs performing k+ 1 turns and k turns for k >= 1. Furthermore, non-recursive trade-offs are shown between arbitrary PDAs and PDAs which perform only a finite number of turns. Finally, several decidability questions are shown to be undecidable and not semidecidable.
We investigate a restricted one-way cellular automaton (OCA) model where the number of cells is bounded by a constant number k, so-called kC-OCAs. In contrast to the general model, the generative capacity of the restricted model is reduced to the set of regular languages. A kC-OCA can be algorithmically converted to a deterministic finite automaton (DFA). The blow-up in the number of states is bounded by a polynomial of degree k. We can exhibit a family of unary languages which shows that this upper bound is tight in order of magnitude. We then study upper and lower bounds for the trade-off when converting DFAs to kC-OCAs. We show that there are regular languages where the use of kC-OCAs cannot reduce the number of states when compared to DFAs. We then investigate trade-offs between kC-OCAs with different numbers of cells and finally treat the problem of minimizing a given kC-OCA.
The effect of adding two-way communication to k cells one-way cellular automata (kC-OCAs) on their size of description is studied. kC-OCAs are a parallel model for the regular languages that consists of an array of k identical deterministic finite automata (DFAs), called cells, operating in parallel. Each cell gets information from its right neighbor only. In this paper, two models with different amounts of two-way communication are investigated. Both models always achieve quadratic savings when compared to DFAs. When compared to a one-way cellular model, the result is that minimum two-way communication can achieve at most quadratic savings whereas maximum two-way communication may provide savings bounded by a polynomial of degree k.
The descriptional complexity of iterative arrays (lAs) is studied. Iterative arrays are a parallel computational model with a sequential processing of the input. It is shown that lAs when compared to deterministic finite automata or pushdown automata may provide savings in size which are not bounded by any recursive function, so-called non-recursive trade-offs. Additional non-recursive trade-offs are proven to exist between lAs working in linear time and lAs working in real time. Furthermore, the descriptional complexity of lAs is compared with cellular automata (CAs) and non-recursive trade-offs are proven between two restricted classes. Finally, it is shown that many decidability questions for lAs are undecidable and not semidecidable.
It is known that deterministic finite automata (DFAs) can be algorithmically minimized, i.e., a DFA M can be converted to an equivalent DFA M' which has a minimal number of states. The minimization can be done efficiently [6]. On the other hand, it is known that unambiguous finite automata (UFAs) and nondeterministic finite automata (NFAs) can be algorithmically minimized too, but their minimization problems turn out to be NP-complete and PSPACE-complete [8]. In this paper, the time complexity of the minimization problem for two restricted types of finite automata is investigated. These automata are nearly deterministic, since they only allow a small amount of non determinism to be used. On the one hand, NFAs with a fixed finite branching are studied, i.e., the number of nondeterministic moves within every accepting computation is bounded by a fixed finite number. On the other hand, finite automata are investigated which are essentially deterministic except that there is a fixed number of different initial states which can be chosen nondeterministically. The main result is that the minimization problems for these models are computationally hard, namely NP-complete. Hence, even the slightest extension of the deterministic model towards a nondeterministic one, e.g., allowing at most one nondeterministic move in every accepting computation or allowing two initial states instead of one, results in computationally intractable minimization problems.
We study the descriptional complexity of cellular automata (CA), a parallel model of computation. We show that between one of the simplest cellular models, the realtime-OCA. and "classical" models like deterministic finite automata (DFA) or pushdown automata (PDA), there will be savings concerning the size of description not bounded by any recursive function, a so-called nonrecursive trade-off. Furthermore, nonrecursive trade-offs are shown between some restricted classes of cellular automata. The set of valid computations of a Turing machine can be recognized by a realtime-OCA. This implies that many decidability questions are not even semi decidable for cellular automata. There is no pumping lemma and no minimization algorithm for cellular automata.
Zellularautomaten sind ein massiv paralleles Berechnungsmodell, das aus sehr vielen identischen einfachen Prozessoren oder Zellen besteht, die homogen miteinander verbunden sind und parallel arbeiten. Es gibt Zellularautomaten in unterschiedlichen Ausprägungen. Beispielsweise unterscheidet man die Automaten nach der zur Verfügung stehenden Zeit, nach paralleler oder sequentieller Verarbeitung der Eingabe oder durch Beschränkungen der Kommunikation zwischen den einzelnen Zellen. Benutzt man Zellularautomaten zum Erkennen formaler Sprachen und betrachtet deren generative Mächtigkeit, dann kann bereits das einfachste zellulare Modell kontextsensitive Sprachen akzeptieren. In dieser Arbeit wird die Beschreibungskomplexität von Zellularautomaten betrachtet. Es wird untersucht, wie sich die Beschreibungsgröße einer formalen Sprache verändern kann, wenn die Sprache mit unterschiedlichen Typen von Zellularautomaten oder sequentiellen Modellen beschrieben wird. Ein wesentliches Ergebnis im ersten Teil der Arbeit ist, daß zwischen zwei Automatenklassen, deren entsprechende Sprachklassen echt ineinander enthalten oder unvergleichbar sind, nichtrekursive Tradeoffs existieren. Das heißt, der Größenzuwachs beim Wechsel von einem Automatenmodell in das andere läßt sich durch keine rekursive Funktion beschränken. Im zweiten Teil der Arbeit werden Zellularautomaten dahingehend beschränkt, daß nur eine feste Zellenzahl zugelassen ist. Zusätzlich werden Automaten mit unterschiedlichem Grad an bidirektionaler Kommunikation zwischen den einzelnen Zellen betrachtet, und es wird untersucht, welche Auswirkungen auf die Beschreibungsgröße unterschiedliche Grade an bidirektionaler Kommunikation haben können. Im Gegensatz zum unbeschränkten Modell können polynomielle und damit rekursive obere Schranken bei Umwandlungen zwischen den einzelnen Modellen bewiesen werden. Durch den Beweis unterer Schranken kann in fast allen Fällen auch die Optimalität der Konstruktionen belegt werden.
We propose a variation of online paging in two-level memory systems where pages in the fast cache get modified and therefore have to be explicitly written back to the slow memory upon evictions. For increased performance, up to alpha arbitrary pages can be moved from the cache to the slow memory within a single joint eviction, whereas fetching pages from the slow memory is still performed on a one-by-one basis. The main objective in this new alpha-paging scenario is to bound the number of evictions. After providing experimental evidence that alpha-paging can adequately model flash-memory devices in the context of translation layers we turn to the theoretical connections between alpha-paging and standard paging. We give lower bounds for deterministic and randomized alpha-paging algorithms. For deterministic algorithms, we show that an adaptation of LRU is strongly competitive, while for the randomized case we show that by adapting the classical Mark algorithm we get an algorithm with a competitive ratio larger than the lower bound by a multiplicative factor of approximately 1.7.
Die Menge digital zur Verfügung stehender Dokumente wächst zunehmend. Umso wichtiger sind adäquate Methoden, um sehr große Dokumentkollektionen durch-suchen zu können. Im Gegensatz zur exakten Suche, bei der nach Dokumenten mit bekannten Dateinamen gesucht wird, werden Techniken des Information Retrieval (IR) dazu eingesetzt, relevante Ergebnisse zu einer Anfrage ausfindig zu machen. Seit einigen Jahren werden verstärkt Kollektionen mit strukturierten Dokumenten durch¬sucht, insbesondere seit Durchsetzung der eXtensible Markup Language (XML) als offizieller Standard des World Wide Web Consortiums (W3C). Mittlerweile gibt es eine Reihe von Forschungsansätzen, bei denen IR-Methoden auf XML-Dokumente angewendet werden. XML Information Retrieval (XML-IR) nutzt dabei die Struktur der Dokumente, um die Suche nach und in denselben effektiver zu machen, d.h. die Qualität von Suchergebnissen zu verbessern, beispielsweise durch Fokussierung auf besonders relevante Dokumentteile. Die bisherigen Lösungen beziehen sich jedoch alle auf zentralisierte Stand-Alone Suchmaschinen zu Forschungszwecken. Sehr große, über eine Vielzahl von Rechnern verteilte Datenkollektionen lassen sich damit nicht durchsuchen. Techniken für verteiltes XML-IR werden in der Praxis auch dort benötigt, wo das zu durchsuchende System aus einer Vielzahl lokaler, heterogener XML-Kollektionen besteht, deren Benutzer ihre Dokumente nicht auf einem zent¬ralen Server speichern wollen oder können; solche Benutzer schließen sich häufig in Form eines dezentralen Peer-to-Peer (P2P) Netzes zusammen. Dennoch gibt es derzeit weder für Systeme im Allgemeinen, noch für P2P-Systeme im Speziellen Suchmaschinen, mit denen nach relevanten Dokumenten gesucht werden kann. In der vorliegenden Dissertation wird daher am Beispiel von P2P-Netzen erstmalig untersucht, inwiefern XML-IR in verteilten Systemen überhaupt effektiv und effizient möglich ist. Dazu wird ein allgemeines Architekturmodell für die Entwick-lung von P2P-Suchmaschinen für XML-Retrieval entworfen, in dem Funktionalität aus den Bereichen XML-IR und P2P in abstrakten Schichten angeordnet ist. Das Modell wird als Grundlage für den Entwurf einer konkreten P2P-Suchmaschine für XML-IR verwendet. Es werden dazu verschiedene Techniken für verteiltes XML-IR entwickelt, um die einzelnen Phasen der Suche umzusetzen: Indizierung der Doku¬mente, Routing der Anfragen, Ranking geeigneter Dokumente und Retrieval von Ergebnissen. Insbesondere die Problematik von aus mehreren Suchbegriffen bestehenden Multitermanfragen sowie Verteilungsaspekte werden berücksichtigt. Neben der zu erzie-lenden Suchqualität steht vor allem der notwendige Kommunikations¬aufwand im Vordergrund. Die entwickelten Methoden werden in Form einer P2P-Suchmaschine für verteiltes XML-Retrieval implementiert, die aus fast 40.000 Zeilen Java-Code besteht. Diese Suchmaschine namens SPIRIX kann voll-funktionsfähig nach XML-Dokumenten in einem P2P-Netz suchen und deren Relevanz inhaltsbasiert bewerten. Für die Kommunikation zwischen Peers wird ein P2P-Protokoll namens SpirixDHT entworfen, das auf Basis von Chord arbeitet und speziell für den Einsatz von XML-IR angepasst wird. Für die Evaluierung der entworfenen Techniken wird zunächst die Suchqualität von SPIRIX nachgewiesen. Dies geschieht durch die Teilnahme an INEX, der internationalen Initiative für die Evaluierung von XML-Retrieval. Im Rahmen von INEX werden jedes Jahr XML-IR Lösungen weltweit miteinander verglichen. Für 2008 konnte mit SPIRIX eine Suchpräzision erreicht werden, die vergleichbar mit der Qualität der Top-10 XML-IR Lösungen ist. In weiteren Experimenten werden die entworfenen Methoden für verteiltes XML-Retrieval mit INEX-Werkzeugen evaluiert; dabei werden jeweils die erzielte Such-qualität und der notwendige Aufwand gegenübergestellt. Die gewonnenen Er¬kenn-tnisse werden auf den Routingprozess angewendet; hier ist speziell die Frage-stellung interessant, wie XML-Struktur zur Performanzverbesserung in Bezug auf die Effizienz eines verteilten Systems genutzt werden kann. Die Evaluierung der konzi¬pier¬ten Routingtechniken zeigt eine signifikante Reduzierung der Anzahl versendeter Nachrichten, ihrer Größe und somit der Netzlast, wobei gleichzeitig eine Steigerung der Suchqualität erreicht wird. Im Rahmen der Dissertation wird somit der Nachweis erbracht, dass verteiltes XML-IR sowohl effektiv als auch effizient möglich ist. Zugleich wird gezeigt, wie die Ver¬wendung von XML-IR Techniken beim Routing der Anfragen dazu beitragen kann, den notwendige Suchaufwand – insbesondere den für die Kommunikation zwischen Peers – so weit zu reduzieren, dass das System auch zu einer großen Anzahl von teil¬nehmenden Peers skaliert und trotzdem eine hohe Suchqualität aufrecht erhalten werden kann.
Poster presentation: The analysis of neuronal processes distributed across multiple cortical areas aims at the identification of interactions between signals recorded at different sites. Such interactions can be described by measuring the stability of phase angles in the case of oscillatory signals or other forms of signal dependencies for less regular signals. Before, however, any form of interaction can be analyzed at a given time and frequency, it is necessary to assess whether all potentially contributing signals are present. We have developed a new statistical procedure for the detection of coincident power in multiple simultaneously recorded analog signals, allowing the classification of events as 'non-accidental co-activation'. This method can effectively operate on single trials, each lasting only for a few seconds. Signals need to be transformed into time-frequency space, e.g. by applying a short-time Fourier transformation using a Gaussian window. The discrete wavelet transform (DWT) is used in order to weight the resulting power patterns according to their frequency. Subsequently, the weighted power patterns are binarized via applying a threshold. At this final stage, significant power coincidence is determined across all subgroups of channel combinations for individual frequencies by selecting the maximum ratio between observed and expected duration of co-activation as test statistic. The null hypothesis that the activity in each channel is independent from the activity in every other channel is simulated by independent, random rotation of the respective activity patterns. We applied this procedure to single trials of multiple simultaneously sampled local field potentials (LFPs) obtained from occipital, parietal, central and precentral areas of three macaque monkeys. Since their task was to use visual cues to perform a precise arm movement, co-activation of numerous cortical sites was expected. In a data set with 17 channels analyzed, up to 13 sites expressed simultaneous power in the range between 5 and 240 Hz. On average, more than 50% of active channels participated at least once in a significant power co-activation pattern (PCP). Because the significance of such PCPs can be evaluated at the level of single trials, we are confident that this procedure is useful to study single trial variability with sufficient accuracy that much of the behavioral variability can be explained by the dynamics of the underlying distributed neuronal processes.
Poster presentation: Introduction The ability of neurons to emit different firing patterns is considered relevant for neuronal information processing. In dopaminergic neurons, prominent patterns include highly regular pacemakers with separate spikes and stereotyped intervals, processes with repetitive bursts and partial regularity, and irregular spike trains with nonstationary properties. In order to model and quantify these processes and the variability of their patterns with respect to pharmacological and cellular properties, we aim to describe the two dimensions of burstiness and regularity in a single model framework. Methods We present a stochastic spike train model in which the degree of burstiness and the regularity of the oscillation are described independently and with two simple parameters. In this model, a background oscillation with independent and normally distributed intervals gives rise to Poissonian spike packets with a Gaussian firing intensity. The variability of inter-burst intervals and the average number of spikes in each burst indicate regularity and burstiness, respectively. These parameters can be estimated by fitting the model to the autocorrelograms. This allows to assign every spike train a position in the two-dimensional space described by regularity and burstiness and thus, to investigate the dependence of the firing patterns on different experimental conditions. Finally, burst detection in single spike trains is possible within the model because the parameter estimates determine the appropriate bandwidth that should be used for burst identification. Results and Discussion We applied the model to a sample data set obtained from dopaminergic substantia nigra and ventral tegmental area neurons recorded extracellularly in vivo and studied differences between the firing activity of dopaminergic neurons in wildtype and K-ATP channel knock-out mice. The model is able to represent a variety of discharge patterns and to describe changes induced pharmacologically. It provides a simple and objective classification scheme for the observed spike trains into pacemaker, irregular and bursty processes. In addition to the simple classification, changes in the parameters can be studied quantitatively, also including the properties related to bursting behavior. Interestingly, the proposed algorithm for burst detection may be applicable also to spike trains with nonstationary firing rates if the remaining parameters are unaffected. Thus, the proposed model and its burst detection algorithm can be useful for the description and investigation of neuronal firing patterns and their variability with cellular and experimental conditions.
Poster presentation: An important challenge in neuroscience is understanding how networks of neurons go about processing information. Synapses are thought to play an essential role in cellular information processing however quantitative and mathematical models of the underlying physiologic processes that occur at synaptic active zones are lacking. We are generating mathematical models of synaptic vesicle dynamics at a well-characterized model synapse, the Drosophila larval neuromuscular junction. This synapse's simplicity, accessibility to various electrophysiological recording and imaging techniques, and the genetic malleability intrinsic to Drosophila system make it ideal for computational and mathematical studies. We have employed a reductionist approach and started by modeling single presynaptic boutons. Synaptic vesicles can be divided into different pools; however, a quantitative understanding of their dynamics at the Drosophila neuromuscular junction is lacking [4]. We performed biologically realistic simulations of high and low release probability boutons [3] using partial differential equations (PDE) taking into account not only the evolution in time but also the spatial structure in two dimensions (the extension to three dimensions will be implemented soon). PDEs are solved using UG, a program library for the calculation of multi-dimensional PDEs solved using a finite volume approach and implicit time stepping methods leading to extended linear equation systems be solvedwith multi-grid methods [3,4]. Numerical calculations are done on multi-processor computers for fast calculations using different parameters in order to asses the biological feasibility of different models. In preliminary simulations, we modeled vesicle dynamics as a diffusion process describing exocytosis as Neumann streams at synaptic active zones. The initial results obtained with these models are consistent with experimental data. However, this should be regarded as a work in progress. Further refinements will be implemented, including simulations using morphologically realistic geometries which were generated from confocal scans of the neuromuscular junction using NeuRA (a Neuron Reconstruction Algorithm). Other parameters such as glutamate diffusion and reuptake dynamics, as well as postsynaptic receptor kinetics will be incorporated as well.
Poster presentation: Introduction Dopaminergic neurons in the midbrain show a variety of firing patterns, ranging from very regular firing pacemaker cells to bursty and irregular neurons. The effects of different experimental conditions (like pharmacological treatment or genetical manipulations) on these neuronal discharge patterns may be subtle. Applying a stochastic model is a quantitative approach to reveal these changes. ...
Poster presentation: Introduction The brain is a highly interconnected network of constantly interacting units. Understanding the collective behavior of these units requires a multi-dimensional approach. The results of such analyses are hard to visualize and interpret. Hence tools capable of dealing with such tasks become imperative. ....
The pathogenesis of nodular lymphocyte–predominant Hodgkin lymphoma (NLPHL) and its relationship to other lymphomas are largely unknown. This is partly because of the technical challenge of analyzing its rare neoplastic lymphocytic and histiocytic (L&H) cells, which are dispersed in an abundant nonneoplastic cellular microenvironment. We performed a genome-wide expression study of microdissected L&H lymphoma cells in comparison to normal and other malignant B cells that indicated a relationship of L&H cells to and/or that they originate from germinal center B cells at the transition to memory B cells. L&H cells show a surprisingly high similarity to the tumor cells of T cell–rich B cell lymphoma and classical Hodgkin lymphoma, a partial loss of their B cell phenotype, and deregulation of many apoptosis regulators and putative oncogenes. Importantly, L&H cells are characterized by constitutive nuclear factor {kappa}B activity and aberrant extracellular signal-regulated kinase signaling. Thus, these findings shed new light on the nature of L&H cells, reveal several novel pathogenetic mechanisms in NLPHL, and may help in differential diagnosis and lead to novel therapeutic strategies.
Background Although current molecular clock methods offer greater flexibility in modelling historical evolutionary events, calibration of the clock with dates from the fossil record is still problematic for many groups. Here we implement several new approaches in molecular dating to estimate evolutionary ages of Lacertidae, an Old World family of lizards with a poor fossil record and uncertain phylogeny. Four different models of rate variation are tested in a new program for Bayesian phylogenetic analysis called TreeTime, based on a combination of mitochondrial and nuclear gene sequences. We incorporate paleontological uncertainty into divergence estimates by expressing multiple calibration dates as a range of probabilistic distributions. We also test the reliability of our proposed calibrations by exploring effects of individual priors on posterior estimates. Results According to the most reliable model, as indicated by Bayes factor comparison, modern lacertids arose shortly after the K/T transition and entered Africa about 45 million years ago, with the majority of their African radiation occurring in the Eocene and Oligocene. Our findings indicate much earlier origins for these clades than previously reported, and we discuss our results in light of paleogeographic trends during the Cenozoic. Conclusions This study represents the first attempt to estimate evolutionary ages of a specific group of reptiles exhibiting uncertain phylogenetic relationships, molecular rate variation and a poor fossil record. Our results emphasize the sensitivity of molecular divergence dates to fossil calibrations, and support the use of combined molecular data sets and multiple, well-spaced dates from the fossil record as minimum node constraints. The bioinformatics program used here, TreeTime, is publicly available, and we recommend its use for molecular dating of taxa faced with similar challenges.
Im heutigen Zahlungsverkehr übernehmen in zunehmendem Maße Zahlungen mit Kreditkarten eine entscheidende Rolle. Entsprechend der Verbreitung dieser Art des Zahlungsverkehrs nimmt ebenfalls der Mißbrauch mit diesem bargeldlosen Zahlungsmittel zu. Um die Verluste, die bei dem Kreditkarteninstitut auf diese Weise entstehen, so weit wie möglich einzudämmen, wird versucht, Mißbrauchstransaktionen bei der Autorisierung der Zahlungsaufforderung zu erkennen. Ziel dieser Diplomarbeit ist es zu bestimmen, in wie weit es möglich ist, illegale Transaktionen aus der Menge von Autorisierungsanfragen mit Hilfe adaptiver Algorithmen aufzudecken. Dabei sollen sowohl Methoden aus dem Bereich des Data-Mining, als auch aus den Bereichen der neuronalen Netze benutzt werden. Erschwerend bei der Mißbrauchsanalyse kommt hinzu, daß die Beurteilung der einzelnen Transaktionen in Sekundenbruchteilen abgeschlossen sein muß, um die hohe Anzahl an Autorisierungsanfragen verarbeiten zu können und den Kundenservice auf Seiten des Benutzers und des Händlers auf diese Weise zu optimieren. Weiter handelt es sich bei einem Großteil der bei der Analyse zu Verfügung stehenden Datensätze um symbolische Daten, also alpha-numerisch kodierte Werte, die stellvertretend für verschiedene Eigenschaften verwendet werden. Nur wenige der Transaktionsdaten sind analoger Natur, weisen also eine Linearität auf, die es erlaubt, "Nachbarschaften" zwischen den Daten bestimmen zu können. Damit scheidet eine reine Analyse auf Basis von neuronalen Netzwerken aus. Diese Problematik führte unter anderem zu dem verfolgten Ansatz. Als Grundlage der Analyse dienen bekannte Mißbrauchstransaktionen aus einem Zeitintervall von ungefähr einem Jahr, die jedoch aufgrund der hohen Anzahl nicht komplett als solche mit den eingehenden Transaktionen verglichen werden können, da ein sequentieller Vergleich zu viel Zeit in Anspruch nähme. Im übrigen würde durch einen einfachen Vergleich nur der schon bekannte Mißbrauch erkannt werden; eine Abstraktion der Erkenntnisse aus den Mißbrauchserfahrungen ist nicht möglich. Aus diesem Grund werden diese Mißbrauchstransaktionen mit Hilfe von Methoden aus dem Bereich des Data-Mining verallgemeinert und damit auf ein Minimum, soweit es die Verläßlichkeit dieser Datensätze zuläßt, reduziert. Desweiteren schließt sich eine Analyse der zu diesem Zeitpunkt noch nicht betrachteten analogen Daten an, um die maximale, enthaltene Information aus den Transaktionsdaten zu beziehen. Dafür werden moderne Methoden aus dem Bereich der neuronalen Netzwerke, sogenannte radiale Basisfunktionsnetze, verwendet. Da eine Mißbrauchsanalyse ohne eine entsprechende Profilanalyse unvollständig wäre, wurde abschließend mit den vorhanden Mitteln auf den zugrunde liegenden Daten in Anlehnung an die bisherige Methodik eine solche Profilauswertung und zeitabhängige Analyse realisiert. Mit dem so implementierten Modell wurde versucht, auf allgemeine Art und Weise, Verhaltens- beziehungsweise Transaktionsmuster einzuordnen und mit bei der Mißbrauchsentscheidung einfließen zu lassen. Aus den vorgestellten Analyseverfahren wurden verschiedene Klassifizierungsmodelle entwickelt, die zu guten Ergebnissen auf den Simulationsdaten führen. Es kann gezeigt werden, daß die Mißbrauchserkennung durch eine kombinierte Anwendung aus symbolischer und analoger Auswertung bestmöglich durchzuführen ist.
FIFO is the most prominent queueing strategy due to its simplicity and the fact that it only works with local information. Its analysis within the adversarial queueing theory however has shown, that there are networks that are not stable under the FIFO protocol, even at arbitrarily low rate. On the other hand there are networks that are universally stable, i.e., they are stable under every greedy protocol at any rate r < 1. The question as to which networks are stable under the FIFO protocol arises naturally. We offer the first polynomial time algorithm for deciding FIFO stability and simple-path FIFO stability of a directed network, answering an open question posed in [1, 4]. It turns out, that there are networks, that are FIFO stable but not universally stable, hence FIFO is not a worst case protocol in this sense. Our characterization of FIFO stability is constructive and disproves an open characterization in [4].
The efficient management of large multimedia databases requires the development of new techniques to process, characterize, and search for multimedia objects. Especially in the case of image data, the rapidly growing amount of documents prohibits a manual description of the images’ content. Instead, the automated characterization is highly desirable to support annotation and retrieval of digital images. However, this is a very complex and still unsolved task. To contribute to a solution of this problem, we have developed a mechanism for recognizing objects in images based on the query by example paradigm. Therefore, the most salient image features of an example image representing the searched object are extracted to obtain a scale-invariant object model. The use of this model provides an efficient and robust strategy for recognizing objects in images independently of their size. Further applications of the mechanism are classical recognition tasks such as scene decomposition or object tracking in video sequences.
For the efficient management of large image databases, the automated characterization of images and the usage of that characterization for searching and ordering tasks is highly desirable. The purpose of the project SEMACODE is to combine the still unsolved problem of content-oriented characterization of images with scale-invariant object recognition and modelbased compression methods. To achieve this goal, existing techniques as well as new concepts related to pattern matching, image encoding, and image compression are examined. The resulting methods are integrated in a common framework with the aid of a content-oriented conception. For the application, an image database at the library of the university of Frankfurt/Main (StUB; about 60000 images), the required operations are developed. The search and query interfaces are defined in close cooperation with the StUB project “Digitized Colonial Picture Library”. This report describes the fundamentals and first results of the image encoding and object recognition algorithms developed within the scope of the project.
The prevention of credit card fraud is an important application for prediction techniques. One major obstacle for using neural network training techniques is the high necessary diagnostic quality: Since only one financial transaction of a thousand is invalid no prediction success less than 99.9% is acceptable. Due to these credit card transaction proportions complete new concepts had to be developed and tested on real credit card data. This paper shows how advanced data mining techniques and neural network algorithm can be combined successfully to obtain a high fraud coverage combined with a low false alarm rate.
Classically, encoding of images by only a few, important components is done by the Principal Component Analysis (PCA). Recently, a data analysis tool called Independent Component Analysis (ICA) for the separation of independent influences in signals has found strong interest in the neural network community. This approach has also been applied to images. Whereas the approach assumes continuous source channels mixed up to the same number of channels by a mixing matrix, we assume that images are composed by only a few image primitives. This means that for images we have less sources than pixels. Additionally, in order to reduce unimportant information, we aim only for the most important source patterns with the highest occurrence probabilities or biggest information called „Principal Independent Components (PIC)“. For the example of a synthetic picture composed by characters this idea gives us the most important ones. Nevertheless, for natural images where no a-priori probabilities can be computed this does not lead to an acceptable reproduction error. Combining the traditional principal component criteria of PCA with the independence property of ICA we obtain a better encoding. It turns out that this definition of PIC implements the classical demand of Shannon’s rate distortion theory.
We study the effect of randomness in the adversarial queueing model. All proofs of instability for deterministic queueing strategies exploit a finespun strategy of insertions by an adversary. If the local queueing decisions in the network are subject to randomness, it is far from obvious, that an adversary can still trick the network into instability. We show that uniform queueing is unstable even against an oblivious adversary. Consequently, randomizing the queueing decisions made to operate a network is not in itself a suitable fix for poor network performances due to packet pileups.
This paper describes a method to treat contextual equivalence in polymorphically typed lambda-calculi, and also how to transfer equivalences from the untyped versions of lambda-calculi to their typed variant, where our specific calculus has letrec, recursive types and is nondeterministic. An addition of a type label to every subexpression is all that is needed, together with some natural constraints for the consistency of the type labels and well-scopedness of expressions. One result is that an elementary but typed notion of program transformation is obtained and that untyped contextual equivalences also hold in the typed calculus as long as the expressions are well-typed. In order to have a nice interaction between reduction and typing, some reduction rules have to be accompanied with a type modification by generalizing or instantiating types.
Motivated by the question of correctness of a specific implementation of concurrent buffers in the lambda calculus with futures underlying Alice ML, we prove that concurrent buffers and handled futures can correctly encode each other. Correctness means that our encodings preserve and reflect the observations of may- and must-convergence. This also shows correctness wrt. program semantics, since the encodings are adequate translations wrt. contextual semantics. While these translations encode blocking into queuing and waiting, we also provide an adequate encoding of buffers in a calculus without handles, which is more low-level and uses busy-waiting instead of blocking. Furthermore we demonstrate that our correctness concept applies to the whole compilation process from high-level to low-level concurrent languages, by translating the calculus with buffers, handled futures and data constructors into a small core language without those constructs.
We show on an abstract level that contextual equivalence in non-deterministic program calculi defined by may- and must-convergence is maximal in the following sense. Using also all the test predicates generated by the Boolean, forall- and existential closure of may- and must-convergence does not change the contextual equivalence. The situation is different if may- and total must-convergence is used, where an expression totally must-converges if all reductions are finite and terminate with a value: There is an infinite sequence of test-predicates generated by the Boolean, forall- and existential closure of may- and total must-convergence, which also leads to an infinite sequence of different contextual equalities.
Driving can be dangerous. Humans become inattentive when performing a monotonous task like driving. Also the risk implied while multi-tasking, like using the cellular phone while driving, can break the concentration of the driver and increase the risk of accidents. Others factors like exhaustion, nervousness and excitement affect the performance of the driver and the response time. Consequently, car manufacturers have developed systems in the last decades which assist the driver under various circumstances. These systems are called driver assistance systems. Driver assistance systems are meant to support the task of driving, and the field of action varies from alerting the driver, with acoustical or optical warnings, to taking control of the car, such as keeping the vehicle in the traffic lane until the driver resumes control. For such a purpose, the vehicle is equipped with on-board sensors which allow the perception of the environment and/or the state of the vehicle. Cameras are sensors which extract useful information about the visual appearance of the environment. Additionally, a binocular system allows the extraction of 3D information. One of the main requirements for most camera-based driver assistance systems is the accurate knowledge of the motion of the vehicle. Some sources of information, like velocimeters and GPS, are of common use in vehicles today. Nevertheless, the resolution and accuracy usually achieved with these systems are not enough for many real-time applications. The computation of ego-motion from sequences of stereo images for the implementation of driving intelligent systems, like autonomous navigation or collision avoidance, constitutes the core of this thesis. This dissertation proposes a framework for the simultaneous computation of the 6 degrees of freedom of ego-motion (rotation and translation in 3D Euclidean space), the estimation of the scene structure and the detection and estimation of independently moving objects. The input is exclusively provided by a binocular system and the framework does not call for any data acquisition strategy, i.e. the stereo images are just processed as they are provided. Stereo allows one to establish correspondences between left and right images, estimating 3D points of the environment via triangulation. Likewise, feature tracking establishes correspondences between the images acquired at different time instances. When both are used together for a large number of points, the result is a set of clouds of 3D points with point-to-point correspondences between clouds. The apparent motion of the 3D points between consecutive frames is caused by a variety of reasons. The most dominant motion for most of the points in the clouds is caused by the ego-motion of the vehicle; as the vehicle moves and images are acquired, the relative position of the world points with respect to the vehicle changes. Motion is also caused by objects moving in the environment. They move independently of the vehicle motion, so the observed motion for these points is the sum of the ego-vehicle motion and the independent motion of the object. A third reason, and of paramount importance in vision applications, is caused by correspondence problems, i.e. the incorrect spatial or temporal assignment of the point-to-point correspondence. Furthermore, all the points in the clouds are actually noisy measurements of the real unknown 3D points of the environment. Solving ego-motion and scene structure from the clouds of points requires some previous analysis of the noise involved in the imaging process, and how it propagates as the data is processed. Therefore, this dissertation analyzes the noise properties of the 3D points obtained through stereo triangulation. This leads to the detection of a bias in the estimation of 3D position, which is corrected with a reformulation of the projection equation. Ego-motion is obtained by finding the rotation and translation between the two clouds of points. This problem is known as absolute orientation, and many solutions based on least squares have been proposed in the literature. This thesis reviews the available closed form solutions to the problem. The proposed framework is divided in three main blocks: 1) stereo and feature tracking computation, 2) ego-motion estimation and 3) estimation of 3D point position and 3D velocity. The first block solves the correspondence problem providing the clouds of points as output. No special implementation of this block is required in this thesis. The ego-motion block computes the motion of the cameras by finding the absolute orientation between the clouds of static points in the environment. Since the cloud of points might contain independently moving objects and outliers generated by false correspondences, the direct computation of the least squares might lead to an erroneous solution. The first contribution of this thesis is an effective rejection rule that detects outliers based on the distance between predicted and measured quantities, and reduces the effects of noisy measurement by assigning appropriate weights to the data. This method is called Smoothness Motion Constraint (SMC). The ego-motion of the camera between two frames is obtained finding the absolute orientation between consecutive clouds of weighted 3D points. The complete ego-motion since initialization is achieved concatenating the individual motion estimates. This leads to a super-linear propagation of the error, since noise is integrated. A second contribution of this dissertation is a predictor/corrector iterative method, which integrates the clouds of 3D points of multiple time instances for the computation of ego-motion. The presented method considerably reduces the accumulation of errors in the estimated ego-position of the camera. Another contribution of this dissertation is a method which recursively estimates the 3D world position of a point and its velocity; by fusing stereo, feature tracking and the estimated ego-motion in a Kalman Filter system. An improved estimation of point position is obtained this way, which is used in the subsequent system cycle resulting in an improved computation of ego-motion. The general contribution of this dissertation is a single framework for the real time computation of scene structure, independently moving objects and ego-motion for automotive applications.
Various concurrency primitives have been added to sequential programming languages, in order to turn them concurrent. Prominent examples are concurrent buffers for Haskell, channels in Concurrent ML, joins in JoCaml, and handled futures in Alice ML. Even though one might conjecture that all these primitives provide the same expressiveness, proving this equivalence is an open challenge in the area of program semantics. In this paper, we establish a first instance of this conjecture. We show that concurrent buffers can be encoded in the lambda calculus with futures underlying Alice ML. Our correctness proof results from a systematic method, based on observational semantics with respect to may and must convergence.
Exported proteases of Helicobacter pylori (H. pylori) are potentially involved in pathogen-associated disorders leading to gastric inflammation and neoplasia. By comprehensive sequence screening of the H. pylori proteome for predicted secreted proteases, we retrieved several candidate genes. We detected caseinolytic activities of several such proteases, which are released independently from the H. pylori type IV secretion system encoded by the cag pathogenicity island (cagPAI). Among these, we found the predicted serine protease HtrA (Hp1019), which was previously identified in the bacterial secretome of H. pylori. Importantly, we further found that the H. pylori genes hp1018 and hp1019 represent a single gene likely coding for an exported protein. Here, we directly verified proteolytic activity of HtrA in vitro and identified the HtrA protease in zymograms by mass spectrometry. Overexpressed and purified HtrA exhibited pronounced proteolytic activity, which is inactivated after mutation of Ser205 to alanine in the predicted active center of HtrA. These data demonstrate that H. pylori secretes HtrA as an active protease, which might represent a novel candidate target for therapeutic intervention strategies.
Erkennung kritischer Zustände von Patienten mit der Diagnose "Septischer Schock" mit einem RBF-Netz
(2000)
Es wurde gezeigt, dass der Arzt mit dem wachsenden RBF-Netz durch die Ausgabe von verlässlichen Warnungen unterstützt werden kann. Wie in der Clusteranalyse erläutert, leiden die Ergebnisse jedoch unter den wenigen Patienten und unter der ungenauen zeitlichen Erfassung der Daten. Da jeder Patient sehr individuelle Zustände annimmt, ist ein größeres Patientenkollektiv notwendig, um eine umfassende Wissensbasis zu lernen. Eine medizinische Nachbearbeitung der Wissensbasis durch die Analyse der Fälle ließe eine weitere Verbesserung des Ergebnisses erwarten. Somit könnten unbekannte Zusammenhänge durch das Lernen aus Beispielen und medizinisches Fachwissen kombiniert werden. Abstraktere Merkmale, die weniger abhängig von individuellen Zuständen sind, könnten eine Klassifikation noch weiter verbessern. Ein Ansatzpunkt ist z.B. die Abweichung der Messwerte vom gleitenden Mittelwert. Dieses Maß ist unempfindlicher gegenüber den individuellen Arbeitspunkten der Patienten und bildet auch die Basis von relativen Abhängigkeiten zwischen zwei Variablen, die in einem weiteren Schritt ebenfalls als Merkmal herangezogen wurden. Obwohl die Verwendung der relativen Abhängigkeiten zwischen zwei Variablen als Merkmal nicht deutlichere oder häufigere Warnungen hervorbringen konnte, weist doch die Clusteranalyse auf eine bessere Verteilung der Patienten hin. Einige Cluster sind besser für die Vorhersage geeignet, als dieses bei einer Clusterung auf Basis der Zustände erreicht werden kann. Unterstützt wird dieses Ergebnis auch durch den größeren Unterschied der Sicherheiten von falschen und richtigen Klassifikationen. Neben den bisher untersuchten Merkmalen scheinen auch die Variablen interessant zu sein, bei denen festgestellt wurde, dass sie sich trotz Medikamentengabe und adäquater Behandlung schwer stabilisieren lassen. Durch den behandelnden Arzt werden diese Werte üblicherweise in einem gewissen Bereich gehalten. Falls sich das Paar Medikament/physiologischer Parameter nicht mehr in einem sinnvollen Verhältnis befindet, kann dieses ein wichtiger Indikator sein. Nach dem Aufbau der grundlegenden Funktionalität der hier untersuchten Methoden ist die Suche nach geeigneten Merkmalen als Eingabe für ein neuronales Netz ein wesentlicher Bestandteil folgender Arbeiten. Abgesehen von dem generell anspruchsvollen Vorhaben aus Klinikdaten deutliche Hinweise für die Mortalität septischer-Schock-Patienten zu erhalten, liegen die wesentlichen Probleme in dem Umfang und der Messhäufigkeit der Frankfurter Vorstudie begründet, so dass eine Anwendung von Klassifikationsverfahren auf das umfassendere Patientenkollektiv der MEDAN Multicenter-Studie klarere Ergebnisse erwarten lässt. Eine weitere, für medizinische Anwendungen interessante, Analysemöglichkeit ist die Regelgenerierung, die zur Zeit in einem anderen Teilprojekt in der MEDAN-Arbeitsgruppe bearbeitet wird. Hier können im Fall metrischer Daten zusätzliche Hinweise für die Leistung eines reinen Klassifikationsverfahrens gewonnen werden mit dem Vorteil einer expliziten Regelausgabe. Zum anderen werden in diesem Teilprojekt auch Verfahren zur Regelgenerierung eingesetzt, die ordinale und nominale Variablen wie Diagnosen, Operationen, Therapien und Medikamentenangaben (binär, ohne genaue Dosis) auswerten können. Diese werden in den Multicenter-Daten vorhanden sein. Durch Kopplung der Regelgeneratoren für metrische Daten auf der einen Seite und für diskrete Variablen auf der anderen Seite, besteht durchaus die Hoffnung bessere Ergebnisse zu erzielen. Da der Regelgenerator für metrische Daten auf dem RBF-DDA (Abk. für: Dynamic Decay Adjustment)-Netz [BERTHOLD und DIAMOND, 1995] beruht, bietet es sich innerhalb des MEDAN-Projekts an, einen (bislang nicht durchgeführten) Vergleich mit dem hier verwendeten Netztyp durchzuführen. Der Vergleich ist allerdings nur von prinzipiellem Interesse und kann auf den hier betrachteten Daten kein grundsätzlich besseres Ergebnis liefern als die bislang durchgeführten Analysen; er kann aber zu einer umfangreichen Bewertung der Ergebnisse beitragen.
In the context of information theory, the term Mutual Information has first been formulated by Claude Elwood Shannon. Information theory is the consistent mathematical description of technical communication systems. To this day, it is the basis of numerous applications in modern communications engineering and yet became indispensable in this field. This work is concerned with the development of a concept for nonlinear feature selection from scalar, multivariate data on the basis of the mutual information. From the viewpoint of modelling, the successful construction of a realistic model depends highly on the quality of the employed data. In the ideal case, high quality data simply consists of the relevant features for deriving the model. In this context, it is important to possess a suitable method for measuring the degree of the, mostly nonlinear, dependencies between input- and output variables. By means of such a measure, the relevant features could be specifically selected. During the course of this work, it will become evident that the mutual information is a valuable and feasible measure for this task and hence the method of choice for practical applications. Basically and without the claim of being exhaustive, there are two possible constellations that recommend the application of feature selection. On the one hand, feature selection plays an important role, if the computability of a derived system model cannot be guaranteed, due to a multitude of available features. On the other hand, the existence of very few data points with a significant number of features also recommends the employment of feature selection. The latter constellation is closely related to the so called "Curse of Dimensionality". The actual statement behind this is the necessity to reduce the dimensionality to obtain an adequate coverage of the data space. In other word, it is important to reduce the dimensionality of the data, since the coverage of the data space exponentially decreases, for a constant number of data points, with the dimensionality of the available data. In the context of mapping between input- and output space, this goal is ideally reached by selecting only the relevant features from the available data set. The basic idea for this work has its origin in the rather practical field of automotive engineering. It was motivated by the goals of a complex research project in which the nonlinear, dynamic dependencies among a multitude of sensor signals should be identified. The final goal of such activities was to derive so called virtual sensors from identified dependencies among the installed automotive sensors. This enables the real-time computability of the required variable without the expenses of additional hardware. The prospect of doing without additional computing hardware is a strong motive force in particular in automotive engineering. In this context, the major problem was to find a feasible method to capture the linear- as well as the nonlinear dependencies. As mentioned before, the goal of this work is the development of a flexibly applicable system for nonlinear feature selection. The important point here is to guarantee the practicable computability of the developed method even for high dimensional data spaces, which are rather realistic in technical environments. The employed measure for the feature selection process is based on the sophisticated concept of mutual information. The property of the mutual information, regarding its high sensitivity and specificity to linear- and nonlinear statistical dependencies, makes it the method of choice for the development of a highly flexible, nonlinear feature selection framework. In addition to the mere selection of relevant features, the developed framework is also applicable for the nonlinear analysis of the temporal influences of the selected features. Hence, a subsequent dynamic modelling can be performed more efficiently, since the proposed feature selection algorithm additionally provides information about the temporal dependencies between input- and output variables. In contrast to feature extraction techniques, the developed feature selection algorithm in this work has another considerable advantage. In the case of cost intensive measurements, the variables with the highest information content can be selected in a prior feasibility study. Hence, the developed method can also be employed to avoid redundance in the acquired data and thus prevent for additional costs.
We investigate methods and tools for analysing translations between programming languages with respect to observational semantics. The behaviour of programs is observed in terms of may- and must-convergence in arbitrary contexts, and adequacy of translations, i.e., the reflection of program equivalence, is taken to be the fundamental correctness condition. For compositional translations we propose a notion of convergence equivalence as a means for proving adequacy. This technique avoids explicit reasoning about contexts, and is able to deal with the subtle role of typing in implementations of language extension.
The paper proposes a variation of simulation for checking and proving contextual equivalence in a non-deterministic call-by-need lambda-calculus with constructors, case, seq, and a letrec with cyclic dependencies. It also proposes a novel method to prove its correctness. The calculus' semantics is based on a small-step rewrite semantics and on may-convergence. The cyclic nature of letrec bindings, as well as non-determinism, makes known approaches to prove that simulation implies contextual equivalence, such as Howe's proof technique, inapplicable in this setting. The basic technique for the simulation as well as the correctness proof is called pre-evaluation, which computes a set of answers for every closed expression. If simulation succeeds in finite computation depth, then it is guaranteed to show contextual preorder of expressions.
Die Erwartungen von Studieninteressierten weichen häufig beträchtlich von den tatsächlichen Studieninhalten und Anforderungen ab. Ein Grund dafür ist, dass viele sich nicht genügend Klarheit verschaffen, welche eigenen Stärken und Schwächen für den Erfolg in Studium und Beruf »tatsächlich« relevant sind. So könnte zum Beispiel ein Abiturient mit guten Noten in Mathematik und Physik und mäßigen Zensuren in Deutsch und Englisch noch schlussfolgern, dass ihm »das Naturwissenschaftliche mehr liegt«. Ob das naturwissenschaftliche Verständnis für ein erfolgreiches Studium der Informatik jedoch gut genug ausgeprägt ist, lässt sich nicht so leicht erschließen. Noch schwieriger ist es für Studieninteressierte einzuschätzen, wie ihre »Soft Skills« ausgeprägt sind – also die Persönlichkeitsmerkmale, die in der Schule nicht systematisch beurteilt werden, jedoch hochgradig aussagekräftig für langfristigen Erfolg in Studium und Beruf sind. Ein Wechsel des Studienfaches zu Beginn des Studiums führt häufig zu einer Verlängerung der Studiendauer. Auch wenn eine derartige »Orientierungsphase« oftmals als normal und wichtig eingeschätzt wird, zeigt die praktische Erfahrung, dass Studierende mit kurzer Studiendauer jenen, die länger studiert haben, bei der Stellenvergabe tendenziell vorgezogen werden. Eine längere Studiendauer wird von Arbeitgebern häufig als Zeichen mangelnder Zielstrebigkeit oder fehlender Berufsmotivation interpretiert und kann sich so Chancen mindernd für Berufseinsteiger auswirken. Ebenso ist es im Interesse der Universitäten, die Zahl der Studienfachwechsel und -abbrüche so gering wie möglich zu halten – nicht zuletzt aus wirtschaftlichen Gründen. Deshalb bietet die Universität Frankfurt Studieninteressierten – zunächst in den Fächern Informatik und Psychologie – mit dem Self-Assessment konkrete Entscheidungshilfen an. Der verfolgte Ansatz zielt darauf ab, Abiturientinnen und Abiturienten möglichst frühzeitig und mit vertretbarem Aufwand die Möglichkeit zu bieten, selbst zu überprüfen, inwieweit ihre Erwartungen an einen Studiengang mit den tatsächlichen Inhalten und Anforderungen übereinstimmen. Das Konzept zur Erstellung eines Self-Assessments, das hier beispielhaft für den Studiengang Informatik vorgestellt wird, entstand nicht umsonst in enger Kooperation mit dem Institut für Psychologie (Prof. Dr. Helfried Moosbrugger, Dr. Siegbert Reiß, Ewa Jonkisz). Denn neben der fachlichen Qualifikation entscheiden über den Studienerfolg auch persönliche Eigenschaften wie Leistungsbereitschaft und Hartnäckigkeit. Die Auswertung des anonym durchgeführten Self-Assessments deckt außerdem Wissenslücken bei den Studieninteressierten auf, so dass eine gezielte Vorbereitung auf das Studium möglich wird. Zum Beispiel bietet der Fachbereich Mathematik und Informatik gezielte Vorbereitungskurse für Studienanfänger an, und zwar in Programmierung und Mathematik. Auch werden in den Semesterferien Repetitorien und Vorbereitungskurse angeboten – alles aus Studienbeiträgen finanziert. Auf diese Weise kann es zu einem homogeneren Kenntnisstand speziell bei den Studierenden im ersten Semester kommen. Ziel ist es, dadurch auch den »Erstsemesterschock « zu mildern. Das Online-Beratungsangebot trägt damit zu einer direkten Verbesserung der Lern- und Lehrsituation bei.
In der klassischen Theorie der formalen Sprachen gehört die Beschreibung von Sprachen durch Grammatiken oder Automaten zu den wichtigen Themen. Im Gegensatz zu diesen Modellen, die aus einer einzelnen Komponente bestehen, beschäftigt sich die Informatik heute aber immer häufiger mit verteilten Systemen, deren Komponenten auf verschiedene Art und Weise zusammenarbeiten. Eine Möglichkeit, dieses Konzept auf die Theorie der formalen Sprachen zu übertragen, ist die Definition von Grammatiksystemen. Ein Grammatiksystem besteht aus mehreren Grammatiken, die nach bestimmten Regeln zusammenarbeiten. Hauptsächlich unterscheidet man dabei zwischen sequentieller und paralleler Kooperation. In dieser Arbeitwerden kontextfreie „cooperating distributed“ (CD) Grammatiksysteme, ein Modell mit sequentieller Kooperation, betrachtet. Zur Erzeugung eines Wortes arbeiten dabei mehrere kontextfreie Grammatiken, die Komponenten, an einer gemeinsamen Satzform. Zu jedem Zeitpunkt ist immer nur eine einzige Komponente aktiv. Der Schwerpunkt der Arbeit liegt auf der Beschreibungskomplexität von CD Grammatiksystemen. Dabei wird zuerst auf die verschiedenen Maße für die Größe oder statische Komplexität eines CD Grammatiksystems eingegangen. Ein wichtiges Ergebnis im ersten Teil der Arbeit ist, daß man für CD Grammatiksysteme und insbesondere hybride CD Grammatiksysteme, eine Verallgemeinerung von kontextfreien CD Grammatiksystemen, einige dieser Maße nach oben beschränken kann. Darunter fallen die Anzahl der Komponenten und die maximale Anzahl von Produktionen in einer Komponente. Hält man einen der beiden Parameter fest, so entsteht eine unendliche Hierarchie über dem anderen Parameter. Der zweite Teil der Arbeit konzentriert sich darauf, Ergebnisse für Größenmaße zu erzielen, die nicht nur einzelne Aspekte der Komplexität, sondern die gesamte Größe oder Länge eines CD Grammatiksystems darstellen. Dafür werden CD Grammatiksysteme geeignet eingeschränkt. Man erhält metalineare Systeme und Systeme von endlichem Index. Im Gegensatz zum unbeschränkten Modell kann hier die generative Mächtigkeit sehr genau charakterisiert werden und es können Hilfsmittel wie Pumpinglemmata gezeigt werden.Weitere Resultate sind eine unendliche Hierarchie über der Breite beziehungsweise dem Index solcher Grammatiksysteme. Das wesentliches Resultat im zweiten Teil dieser Arbeit besteht daraus, daß zwischen zwei Klassen von diesen eingeschränkten CD Grammatiksystemen, deren entsprechende Sprachklassen echt ineinander enthalten sind, nichtrekursive Tradeoffs existieren. Das heißt, daß sich der Größenzuwachs beim Wechsel von der stärkeren Klasse von CD Grammatiksystemen in die schwächere durch keine rekursive Funktion beschränken läßt.
The goal of this report is to prove correctness of a considerable subset of transformations w.r.t. contextual equivalence in a an extended lambda-calculus with case, constructors, seq, let, and choice, with a simple set of reduction rules. Unfortunately, a direct proof appears to be impossible. The correctness proof is by defining another calculus comprising the complex variants of copy, case-reduction and seq-reductions that use variablebinding chains. This complex calculus has well-behaved diagrams and allows a proof that of correctness of transformations, and also that the simple calculus defines an equivalent contextual order.
Das Bumpmapping-Verfahren, eine Methode zur realistischen Darstellung rauer Oberflächen, existiert schon seit 30 Jahren, aber erst durch aktuelle Entwicklungen der Hardware lässt es sich in Echtzeitumgebungen einsetzen. Die aktuellen Verfahren ermöglichen viele darüber hinausgehende Effekte, jedoch haben sie auch mit Problemen zu kämpfen. Das Ziel dieser Diplomarbeit ist die Weiterentwicklung der Verfahren zu betrachten. In dieser Arbeit werden die Grenzen der aktuellen Bumpmapping-Algorithmen aufgezeigt und nach neuen Wegen geforscht. Das erste Verfahren erzeugt durch ein Multipassrendern fraktale Landschaften im Shader. Die darin verwendeten Methoden lassen sich für einen weiteren Algorithmus nutzen, mit dem feine Unebenheiten der Oberfläche an jedem Pixel ausgewertet werden. So können anisotrope Materialien wie gebürstete Metalle oder Mikropartikellacke simuliert werden. Den Abschluss bilden zwei neue Verfahren für prozedurale Shader. Die zu imitierende Oberfläche wird im Modell nachgebildet und per Raytracing für jeden Oberflächenpixel ausgewertet. Durch diese Methode werden viele Probleme texturbasierter Verfahren komplett umgangen.