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)
In this dissertation a non-deterministic lambda-calculus with call-by-need evaluation is treated. Call-by-need means that subexpressions are evaluated at most once and only if their value must be known to compute the overall result. Also called "sharing", this technique is inevitable for an efficient implementation. In the lambda-ND calculus of chapter 3 sharing is represented explicitely by a let-construct. Above, the calculus has function application, lambda abstractions, sequential evaluation and pick for non-deterministic choice. Non-deterministic lambda calculi play a major role as a theoretical foundation for concurrent processes or side-effected input/output. In this work, non-determinism additionally makes visible when sharing is broken. Based on the bisimulation method this work develops a notion of equality which respects sharing. Using bisimulation to establish contextual equivalence requires substitutivity within contexts, i.e., the ability to "replace equals by equals" within every program or term. This property is called congruence or precongruence if it applies to a preorder. The open similarity of chapter 4 represents a new concept, insofar that the usual definition of a bisimulation is impossible in the lambda-ND calculus. So in section 3.2 a further calculus lambda-Approx has to be defined. Section 3.3 contains the proof of the so-called Approximation Theorem which states that the evaluation in lambda-ND and lambda-Approx agrees. The foundation for the non-trivial precongruence proof is set out in chapter 2 where the trailblazing method of Howe is extended to be capable with sharing. By the use of this (extended) method, the Precongruence Theorem proves open similarity to be a precongruence, involving the so-called precongruence candidate relation. Joining with the Approximation Theorem we obtain the Main Theorem which says that open similarity of the lambda-Approx calculus is contained within the contextual preorder of the lambda-ND calculus. However, this inclusion is strict, a property whose non-trivial proof involves the notion of syntactic continuity. Finally, chapter 6 discusses possible extensions of the base calculus such as recursive bindings or case and constructors. As a fundamental study the calculus lambda-ND provides neither of these concepts, since it was intentionally designed to keep the proofs as simple as possible. Section 6.1 illustrates that the addition case and constructors could be accomplished without big hurdles. However, recursive bindings cannot be represented simply by a fixed point combinator like Y, thus further investigations are necessary.
Ziel dieser Arbeit war es, ein System zu entwickeln, mit dem Sätze von Reduktionsdiagrammen auf ihre Vollständigkeit überprüft werden können. Das System sollte in der puren, funktionalen Programmiersprache Haskell realisiert werden und speziell auf einen nichtdeterministischen Kalkül mit Konstruktoren, einem case-Konstrukt und einem rekursiven let- Ausdruck (letrec) ausgerichtet sein. Dazu wurde in Kapitel 2 der lambda-Kalkül und funktionale Programmiersprachen eingeführt, um die Entwicklung der Kalküle lambda-nd und lambda-nd,rec zu motivieren. Die Basis-Kalküle lambda-nd und lamda-nd,rec wurden in Kapitel 3 bezüglich ihrer Sprachdefinition und Reduktionsregeln vorgestellt. Die Implementierung der beiden Kalküle und der Parser für die verwendete Kernsprache wurden ebenso angegeben wie die Mechanismen zur Markierung und Reduktion der Terme. Die Unterscheidung eines reduzierbaren Terms in NO- und internen Redex, sowie deren Erkennung wurde in diesem Kapitel besonders herausgestellt, da sie die Grundlage für die zu validierenden Reduktionsdiagramme darstellt. Damit ist der Grundstock für diese Arbeit gelegt worden. In Kapitel 4 haben wir kurz Methoden vorgestellt, die lamda-Kalkülen und deren Derivate eine Bedeutung zuzumessen versuchen, um Programme oder Terme miteinander vergleichen zu können. Also nicht nur ihre Termstruktur, sondern ihr Verhalten zu vergleichen. Dabei ist festgestellt worden, daß für nichtdeterministische Kalküle nur eine Methode verfügbar ist, und zwar die der kontextuellen Äquivalenz. Da wir gängige Programmtransformationen dahingehend überprüfen wollten, ob sie der kontextuellen Äquivalenz genügen, also nicht die Auswertung oder das Ergebnis derselben verändern, haben wir ein Kontext-Lemma vorgestellt. Mit Hilfe des Kontext-Lemmas ist es uns möglich gewesen, die Gültigkeit von Beweisen in Reduktionskontexten auf beliebige Kontexte auszudehnen. Für die eigentlichen Beweise werden Reduktionsdiagramme benötigt, die Reduktionsfolgen in verschiedener Weise umstellen. Wir haben die Reduktionsdiagramme ebenfalls in Kapitel 4 definiert. Die Reduktionsdiagramme müssen an jeder Stelle einer Reduktionsfolge anwendbar sein, da sonst die Äquivalenz-Beweise nicht möglich sind. D. h. es müßte bewiesen werden, daß mindestens ein Reduktionsdiagramm einer definierten Menge von Reduktionsdiagrammen für jeden Term und jede seiner Reduktionsfolgen anwendbar ist. Der naive Weg wäre, alle Terme und seine Reduktionsfolgen dahingehend zu überprüfen. Da dies jedoch nicht möglich ist, haben wir uns dazu entschlossen so viele Terme wie möglich zu untersuchen, nicht um die Vollständigkeit der Diagramme zu beweisen, sondern um zu zeigen, daß auf viele verschiedenartige Terme Reduktionsdiagramme erfolgreich angewendet werden können. Die Generierung der Terme haben wir in Kapitel 5 ausführlich dargestellt. In Kapitel 6 haben wir die Sprache zur Darstellung von Reduktionsdiagrammen und die Implementierung der Diagramm-Validierung beschrieben. Weiterhin haben wir ein Verfahren vorgestellt, mit dem wir fehlende Diagramme für Terme suchen und meist auch finden können. Das gesamte System haben wir so aufgebaut, daß eine große Menge an Termen generiert wird, für die Diagramme anwendbar sein müssen. Wenn keines der Diagramme auf einen Term anwendbar ist, also nicht validiert werden kann, dann wird ein passendes Diagramm gesucht. Mit Hilfe des entwickelten Systems Jonah sind in Kapitel 7 verschiedene Programmtransformationen dahingehend überprüft worden, ob die angegebenen Reduktionsdiagramme für große Mengen von Termen gültig sind. Dabei ist als Ergebnis herausgekommen, daß ein vollständiger Satz an Reduktionsdiagrammen für die (cp)-Reduktion nur sehr schwer zu finden ist. Selbst neu hinzugefügte Transformationen, die dabei helfen sollten, die Schwierigkeiten zu umgehen, konnten nicht verwendet werden, da es uns ebenfalls nicht möglich gewesen ist, für sie vollständige Diagrammsätze zu finden. Daraufhin haben wir den Basis-Kalkül zweimal erweitert, um die Schwierigkeiten der (cp)-Diagramme in den Griff zu bekommen. Aber auch diese Ansätze haben kein zufriedenstellendes Ergebnis geliefert. Als positives Ergebnis dieser Arbeit kann aber festgestellt werden, daß das System Jonah bei der Entwicklung nichtdeterministischer Kalküle auf Basis von lambda-Kalkülen eine sehr gute Hilfestellung sein kann, auch wenn es nicht zum vollständigen Beweis der Gültigkeit von Reduktionsdiagrammen dienen kann.
In dieser Diplomarbeit wurde zunächst eine Einführung in das Gebiet der Unifikationstheorie gegeben, um dann zum Teilgebiet des Kontextmatchings zu kommen. Dieses wurde in das Gesamtgebiet der Unifikation eingeordnet. In Anlehnung an [Schm2003] wurde die Komplexität einiger Einschränkungen des Kontextmatchings betrachtet. Insbesondere wurde ein Algorithmus zur Lösung linearer Kontextmatchingprobleme in polynomieller Zeit vorgestellt. Es folgte die Einführung des Transformationsalgorithmus aus [Schm2003] zur Lösung allgemeiner Kontextmatchingprobleme, wobei nach und nach verbesserte Transformationsregeln für einzelne spezielle Problemsituationen vorgestellt wurden. Über [Schm2003] hinausgehend wurden die Regeln Split: Korrespondierende Lochpfade und Konstantenelimination vorgestellt. Im Rahmen der Diplomarbeit wurden die genannten Algorithmen in der funktionalen Programmiersprache Haskell implementiert, wobei auf eine einfache Erweiterbarkeit um neue Transformationsregeln sowie alternative Heuristiken zur Auswahl der in einem Schritt anzuwendenden Transformationsregel geachtet wurde. Die Implementierung (und damit auch die in ihr implementierten Algorithmen) wurde mit Hilfe von zufällig erzeugten Termen auf ihre Leistungsfähigkeit getestet. Hauptaugenmerk lag dabei darauf, inwiefern sich Regeln, die über die Basisregeln aus Tabelle 3.4.1 hinausgehen, positiv auf die Anzahl der Transformationsschritte auswirken. Das Ergebnis ist beeindruckend: durch die Einführung komplexerer Transformationsregeln ließen sich in unseren Testfällen bis zu 87% der Transformationsschritte einsparen, im Durchschnitt immerhin noch 83%. Speziell komplexere Kontextmatchingprobleme mit einer größeren Anzahl an Kontextvariablen profitieren hiervon. Insbesondere die Erkennung korrespondierender Positionen in Verbindung mit der Regel Split führte zu erheblichen Verbesserungen. Die implementierten Algorithmen zur Erkennung korrespondierender Positionen stellen teilweise nur ein notwendiges Kriterium für die Existenz korrespondierender Löcher dar. Dies kann zu fehlerhaften Erkennungen solcher Positionen führen. Wie sich in unseren Tests zeigte, scheint das jedoch kein gravierendes Problem zu sein, da die entsprechenden Split- Transformationen ohnehin äußerst sparsam eingesetzt werden.
Wir haben ein Softwaresystem entwickelt, das in der Lage ist, Beschreibungen von Termersetzungssystemen höherer Ordnung, deren Reduktionsregeln auf einer strukturellen operationalen Semantik basieren, einzulesen und zu interpretieren. Das System ist dabei fähig, Reduktionskontexte für die Redexsuche zu benutzen, die entweder vom Benutzer definiert werden können oder automatisch anhand der strikten Positionen berechnet werden. Außerdem dürfen Kontexte und spezielle Definitionen für Term-Mengen, die wir Domains nennen, in den Reduktionsregeln verwendet werden. Mit dem resultierenden Reduktionssystem-Format können wir somit nicht nur den „lazy“ Lambda-Kalkül, den Call-by-Value Lambda-Kalkül und verwandte, um Konstruktoren und Fallunterscheidungen erweiterte Kalküle, wie die in Kapitel 4 vorgestellten Kernsprachen KFP und PCF, darstellen, sondern auch den (in Abschnitt 4.3 vorgestellten) Call-by-Need Lambda-Kalkül, welcher sich durch die Verwendung von Kontexten innerhalb der Regeln deutlich von den anderen Kalkülen abhebt. Allerdings hält sich der Call-by-Need Lambda-Kalkül damit nicht an das in Kapitel 5 vorgestellte GDSOS-Format, das u.a. sicherstellt, dass Bisimulation eine Kongruenz ist. Wir haben dabei in Abschnitt 5.3.3 bewiesen, dass sich ein GDSOS-Reduktionssystem in ein äquivalentes strukturiertes Auswertungssystem nach Howe übersetzen lässt. Unser System ist in der Lage, die GDSOS-Bedingungen zu prüfen und gibt eine Warnung aus, falls eine der nötigen Bedingungen nicht erfüllt ist (wobei aus dieser auch gleich der Grund des Verstoßes hervorgeht). Wie wir gesehen haben, ist unser System nicht nur befähigt, die einzelnen Reduktionsschritte für kleinere Bespiele ordnungsgemäß auszuführen, sondern es ist durchaus in der Lage, auch aufwendigere KFP-Ausdrücke, wie in unserem Quicksort- Beispiel, auszuwerten.
A new approach to optimize multilevel logic circuits is introduced. Given a multilevel circuit, the synthesis method optimizes its area while simultaneously enhancing its random pattern testability. The method is based on structural transformations at the gate level. New transformations involving EX-OR gates as well as Reed–Muller expansions have been introduced in the synthesis of multilevel circuits. This method is augmented with transformations that specifically enhance random-pattern testability while reducing the area. Testability enhancement is an integral part of our synthesis methodology. Experimental results show that the proposed methodology not only can achieve lower area than other similar tools, but that it achieves better testability compared to available testability enhancement tools such as tstfx. Specifically for ISCAS-85 benchmark circuits, it was observed that EX-OR gate-based transformations successfully contributed toward generating smaller circuits compared to other state-of-the-art logic optimization tools.
Retiming is a widely investigated technique for performance optimization. It performs powerful modifications on a circuit netlist. However, often it is not clear, whether the predicted performance improvement will still be valid after placement has been performed. This paper presents a new retiming algorithm using a highly accurate timing model taking into account the effect of retiming on capacitive loads of single wires as well as fanout systems. We propose the integration of retiming into a timing-driven standard cell placement environment based on simulated annealing. Retiming is used as an optimization technique throughout the whole placement process. The experimental results show the benefit of the proposed approach. In comparison with the conventional design flow based on standard FEAS our approach achieved an improvement in cycle time of up to 34% and 17% on the average.
Retiming is a widely investigated technique for performance optimization. In general, it performs extensive modifications on a circuit netlist, leaving it unclear, whether the achieved performance improvement will still be valid after placement has been performed. This paper presents an approach for integrating retiming into a timing-driven placement environment. The experimental results show the benefit of the proposed approach on circuit performance in comparison with design flows using retiming only as a pre- or postplacement optimization method.
Channel routing is an NP-complete problem. Therefore, it is likely that there is no efficient algorithm solving this problem exactly.In this paper, we show that channel routing is a fixed-parameter tractable problem and that we can find a solution in linear time for a fixed channel width.We implemented our approach for the restricted layer model. The algorithm finds an optimal route for channels with up to 13 tracks within minutes or up to 11 tracks within seconds.Such narrow channels occur for example as a leaf problem of hierarchical routers or within standard cell generators.
We present a theoretical analysis of structural FSM traversal, which is the basis for the sequential equivalence checking algorithm Record & Play presented earlier. We compare the convergence behaviour of exact and approximative structural FSM traversal with that of standard BDD-based FSM traversal. We show that for most circuits encountered in practice exact structural FSM traversal reaches the fixed point as fast as symbolic FSM traversal, while approximation can significantly reduce in the number of iterations needed. Our experiments confirm these results.
We present the FPGA implementation of an algorithm [4] that computes implications between signal values in a boolean network. The research was performed as a masterrsquos thesis [5] at the University of Frankfurt. The recursive algorithm is rather complex for a hardware realization and therefore the FPGA implementation is an interesting example for the potential of reconfigurable computing beyond systolic algorithms. A circuit generator was written that transforms a boolean network into a network of small processing elements and a global control logic which together implement the algorithm. The resulting circuit performs the computation two orders of magnitudes faster than a software implementation run by a conventional workstation.
This paper presents a new timing driven approach for cell replication tailored to the practical needs of standard cell layout design. Cell replication methods have been studied extensively in the context of generic partitioning problems. However, until now it has remained unclear what practical benefit can be obtained from this concept in a realistic environment for timing driven layout synthesis. Therefore, this paper presents a timing driven cell replication procedure, demonstrates its incorporation into a standard cell placement and routing tool and examines its benefit on the final circuit performance in comparison with conventional gate or transistor sizing techniques. Furthermore, we demonstrate that cell replication can deteriorate the stuck-at fault testability of circuits and show that stuck-at redundancy elimination must be integrated into the placement procedure. Experimental results demonstrate the usefulness of the proposed methodology and suggest that cell replication should be an integral part of the physical design flow complementing traditional gate sizing techniques.
One of the most severe short-comings of currently available equivalence checkers is their inability to verify integer multipliers. In this paper, we present a bit level reverse-engineering technique that can be integrated into standard equivalence checking flows. We propose a Boolean mapping algorithm that extracts a network of half adders from the gate netlist of an addition circuit. Once the arithmetic bit level representation of the circuit is obtained, equivalence checking can be performed using simple arithmetic operations. Experimental results show the promise of our approach.
We present new concepts to integrate logic synthesis and physical design. Our methodology uses general Boolean transformations as known from technology-independent synthesis, and a recursive bi-partitioning placement algorithm. In each partitioning step, the precision of the layout data increases. This allows effective guidance of the logic synthesis operations for cycle time optimization. An additional advantage of our approach is that no complicated layout corrections are needed when the netlist is changed.
We study queueing strategies in the adversarial queueing model. Rather than discussing individual prominent queueing strategies we tackle the issue on a general level and analyze classes of queueing strategies. We introduce the class of queueing strategies that base their preferences on knowledge of the entire graph, the path of the packet and its progress. This restriction only rules out time keeping information like a packet’s age or its current waiting time.
We show that all strategies without time stamping have exponential queue sizes, suggesting that time keeping is necessary to obtain subexponential performance bounds. We further introduce a new method to prove stability for strategies without time stamping and show how it can be used to completely characterize a large class of strategies as to their 1-stability and universal stability.
In der vorliegenden Diplom-Arbeit wurde das in [19] vorgeschlagene Modell zur Partitionierung hybrider Systeme diskutiert und die Anwendbarkeit verschiedener verschiedener Optimierungsverfahren auf das Problem untersucht.
Hierbei wurde der Systemgraph um die Ein-/Ausgabe-Blöcke erweitert, damit der Systemgraph eine eine konsistente Erweiterung des des Graphen-Modells darstellt. Weiterhin wurden die Probleme und Einschränkungen aufgezeigt, die sich bei der Abbildung eines hybriden Systems auf den Systemgraphen ergeben.
The thesis in general deals with CORBA, the Common Object Request Broker Architecture. More specifically, it takes a look at the server-side, where object adapters exist to aid the developer in implementing objects and in dealing with request processing. The new Portable Object Adapter was recently added to the CORBA 2.2 standard. My task was the implementation of the POA in MICO and the examination if (a) the POA specification is sensible and (b) in which areas it improves over the old Basic Object Adapter. After introducing distributed platforms in general and CORBA in particular, the thesis' main two chapters are a detailed abstract examination ("Design") of the POA design and their relization ("Implementation"), highlighting the potential trouble spots, persistence and collocation.
Wir betrachten das auf der Crypto '97 vorgeschlagene gitterbasierte Kryp- tosystem von Goldreich, Goldwasser und Halevi (GGH) [11]. Die Autoren veröffentlichten Challenges zu den Sicherheitsparametern 200, 250, 300, 350 und 400 [12]. Jeder Challenge besteht aus dem öffentlichen Schlüssel, sowie einem Ciphertext. Für den Angriff entwickeln wir numerisch stabile Gitterreduktionsalgorithmen, die es ermöglichen, das System in diesen Dimensionen anzugreifen. Es werden Methoden zur Orthogonalisierung, die sogenannten House- holder-Reflexionen und Givens-Rotationen behandelt, und eine praktikable Gleitpunkt-Arithmetik Version des LLL-Algorithmus nach Lenstra, Lenstra und Lov'asz [16] angegeben. Wir entwickeln und analysieren den LLL-Block- Algorithmus, der die Gitterreduktion in Blöcken organisiert. Die Gleitpunkt-Arithmetik Version des LLL-Block-Algorithmus wird experimentell auf das GGH-Schema angewendet und mit der LLL-Reduktion in den Dimensio- nen 100 bis 400 verglichen. Neben der besseren numerischen Stabilität ist die LLL-Block-Reduktion um den Faktor 10 bis 18 mal schneller als die gewöhnliche LLL-Reduktion. Das GGH-Kryptosystem wurde ebenfalls von Nguyen [22] angegriffen, und die ursprünglichen Nachrichten wurden bis in Dimension 350 rekonstruiert. Wir stellen weitere Angriffe auf das Kryptosystem vor. Es zeigt sich, dass die öffentlichen Parameter für erfolgreiche Angriffe benutzt werden können. Der private Schlüssel in der Dimension 200 wird nach ca. 10 Stunden rekonstruiert und Ciphertext-Attaken sind bis in Dimension 300 erfolgreich.
Um in verschiedenen Anwendungsumgebungen eingesetzt werden zu können, lässt die CORBA-Spezifikation einen weiten Spielraum für Implementierungen. Sollte CORBA in einem speziellen Umfeld eingesetzt werden, so war bisher eine Neu-Implementierung notwendig, da herkämmliche CORBA-Implementierungen nicht oder nur sehr eingeschränkt an spezielle Anwendungsumgebungen anpassbar sind. In dieser Arbeit wurde ein Ansatz für eine erweiterbare CORBA-Implementierung vorgestellt und implementiert.
This thesis has explored how structural techniques can be applied to the problem of formal verification for sequential circuits. Algorithms for formal verification which operate on non-canonical gate netlist representations of digital circuits have certain advantages over the traditional techniques based on canonical representations as BDDs. They allow to exploit problem-specific knowledge because they can take into account structural properties of the designs being analyzed. This allows us to break the problem down into sub-problems which are (hopefully) easier to be solved. However, in the past, the main application of such structural techniques was in the field of combinational equivalence checking. One reason for this is that the behaviour of a sequential system does not only depend on its inputs but also on its internal states, and no concepts had been developed to-date allowing structural methods to deal with large sets of states. An important goal of this research was therefore to develop structural, non-canonical forms of representing the reachable states of a finite state machine and to develop methods for reachability analysis based on such representations. In order to reach this goal, two steps were taken. Firstly, a framework for manipulating Boolean functions represented as gate netlists has been established. Secondly, using this framework, a structural method for FSM traversal was developed serving as the basis for an equivalence checking algorithm for sequential circuits. The framework for manipulating Boolean functions represented as multi-level combinational networks is based on a new concept of an implicant in a multi-level network and on an AND/ORtype enumeration technique which allows us to derive such implicants. This concept extends the classical notion of an implicant in two-level circuits to the multi-level case. Using this notion, arbitrary transformations in multi-level combinational networks can be performed. The multi-level network implicants can be determined from AND/OR reasoning graphs, which are associated with an AND/OR reasoning technique operating directly on the gate netlist description of a multi-level circuit. This reasoning technique has the important property that it is complete, i.e. the associated AND/OR trees contain all prime implicants of a Boolean function at an arbitrary node in a combinational circuit. In other words, AND/OR graphs constructed for a network function serve as a representation of this function. A great advantage over BDDs is that AND/OR graphs, besides representing the logic function, also represent some structural properties of the analyzed circuitry. This permits to develop heuristics that are specially tailored for certain applications such as logic optimization or verification. Another advantage which is especially useful for logic optimization is the fact that the proposed AND/OR enumeration scheme is not restricted to the use of a specific logic alphabet such as B3 = {0, 1, X}. By using Roth’s D-calculus based on B5 = {0, 1, D, D-Komplement} permissible implicants can be determined. Transformations based on permissible implicants exploit observability don’t-care conditions in logic synthesis by creating permissible functions at internal network nodes. In order to evaluate the new structural framework for manipulating Boolean functions represented as gate netlists, several experiments with implicant-based optimization of multi-level circuits were performed. The results show that implicant-based circuit transformations lead to significantly better optimization results than traditional synthesis techniques. Next, based on the proposed structural methods for Boolean function manipulation, techniques for representing and manipulating the set of states of a sequential circuit have been developed. The concept of a “stub circuit” was introduced which implicitly represents a set of state vectors as the range of a multi-output function given as a gate netlist. The stub circuit is the result of an existential quantification operation which is obtained by functional decomposition using implicant-based netlist transformations and a network cutting procedure. Using this existential quantification operation, a new structural FSM traversal algorithm was formulated which performs a fixed point iteration on the set of reachable states represented by the stub circuit. The proposed approach performs a reachability analysis of the states of a sequential circuit. It operates on gate netlists and naturally allows to incorporate structural properties of a design under consideration into the reasoning. Therefore, structural FSM traversal is an interesting alternative to traditional symbolic FSM traversal, especially in those applications of formal verification, where structural properties can be exploited. Structural FSM traversal was applied to the problem of sequential equivalence checking. Here, structural similarities between the designs to be compared can effectively reduce the complexity of the verification task. The FSM to be traversed is a special product machine called sequential miter. The special structural properties of this product machine have made it possible to formulate an approximate algorithm for structural FSM traversal, called record and play(). This algorithm uses an approximation on the reachable state set represented by the stub circuit which is very beneficial for performance. Instead of calculating the stub circuit using the exact algorithm, implicant-based transformations directly using structural design similarities are performed. These transformations, together with existential quantification implemented by the cutting procedure, lead to an over-approximation of the reachable state set. By this overapproximation, only such unreachable product states are added to the set of states represented by the stub circuit which are unreachable at the current point in time but which are nevertheless equivalent. Therefore, more product states are added to the set of reachable states sometimes leading to drastic acceleration of the traversal, i.e. the fixed point is reached in much fewer steps. The algorithm record and play() was applied to the problem of checking the equivalence of a circuit with its optimized and retimed version. Retiming is a form of sequential circuit optimization which can radically alter the state encoding of a circuit. Traditional FSM traversal techniques often fail because the BDDs needed to represent the reachable state set and the transition relation of the product machine become too large. Experiments were conducted to evaluate the performance of record and play() on a standard set of sequential benchmark circuits. The algorithm was capable of proving the equivalence of optimized and retimed circuits with their original versions, some of which (to our knowledge) have never before been verified using traditional techniques like symbolic FSM traversal. The experimental results are very promising. Future research will therefore explore how structural FSM traversal can be applied to model checking.
Analyse von Heuristiken
(2006)
Heuristiken treten insbesondere im Zusammenhang mit Optimierungsproblemen in Erscheinung, bei solchen Problemen also, bei denen nicht nur eine Lösung zu finden ist, sondern unter mehreren möglichen Lösungen eine in einem objektiven Sinne beste Lösung ausfindig gemacht werden soll. Beim Problem kürzester Superstrings werden Heuristiken herangezogen, da mit exakten Algorithmen in Anbetracht der APX-Vollständigkeit des Problems nicht zu rechnen ist. Gegeben ist eine Menge S von Strings. Gesucht ist ein String s, so dass jeder String aus S Teilstring von s ist. Die Länge von s ist dabei zu minimieren. Die prominenteste Heuristik für das Problem kürzester Superstrings ist die Greedy-Heuristik, deren Approximationsfaktor derzeit jedoch nur unzureichend beschränkt werden kann. Es wird vermutet (die sogenannte Greedy-Conjecture), dass der Approximationsfaktor genau 2 beträgt, bewiesen werden kann aber nur, dass er nicht unter 2 und nicht über 3,5 liegt. Die Greedy-Conjecture ist das zentrale Thema des zweiten Kapitels. Die erzielten Ergebnisse sind im Wesentlichen: * Durch die Betrachtung von Greedyordnungen können bedingte lineare Ungleichungen nutzbar gemacht werden. Dieser Ansatz ermöglicht den Einsatz linearer Programmierung zum Auffinden interessanter Instanzen und eine Vertiefung des Verständnisses solcher schwerer Instanzen. Dieser Ansatz wird eingeführt und eine Interpretation des dualen Problems wird dargestellt. * Für die nichttriviale, große Teilklasse der bilinearen Greedyordnungen wird gezeigt, dass die Länge des von der Greedy-Heuristik gefundenen Superstrings und die des optimalen Superstrings sich höchstens um die Größe einer optimalen Kreisüberdeckung der Strings unterscheiden. Da eine optimale Kreisüberdeckung einer Menge von Strings stets höchstens so groß ist wie ein optimaler Superstring (man schließe einen Superstring zu einem einzelnen Kreis), ist das erzielte Ergebnis für die betrachtete Teilklasse der Greedyordnungen stärker als die klassische Greedy-Conjecture. * Es wird eine neue bedingte lineare Ungleichung auf Strings -- die Tripelungleichung -- gezeigt, die für das eben genannte Hauptergebnis wesentlich ist. * Schließlich wird gezeigt, dass die zum Nachweis der oberen Schranke von 3,5 für den Approximationsfaktor herangezogenen bedingten Ungleichungen (etwa die Monge-Ungleichung) inhärent zu schwach sind, um die Greedy-Conjecture selbst für lineare Greedyordnungen zu beweisen. Also ist die neue Tripelungleichung auch notwendig. Zuletzt wird gezeigt, dass das um die Tripelungleichung erweiterte System bedingter linearer Ungleichungen inhärent zu schwach ist, um die klassische Greedy-Conjecture für beliebige Greedyordnungen zu beweisen. Mit der Analyse von Queueing Strategien im Adversarial Queueing Modell wird auch ein Fall betrachtet, in dem Heuristiken auf Grund von anwendungsspezifischen Forderungen wie Online-Setup und Lokalität eingesetzt werden. Pakete sollen in einem Netzwerk verschickt werden, wobei jeder Rechner nur begrenzte Information über den Zustand des Netzwerks hat. Es werden Klassen von Queueing Strategien untersucht und insbesondere untersucht, wovon Queueing Strategien ihre lokalen Entscheidungen abhängig machen sollten, um ein gewisses Qualitätsmerkmal zu erreichen. Die hier erzielten Ergebnisse sind: * Jede Queueing Strategie, die ohne Zeitstempel arbeitet, kann zu einer exponentiell großen Queue und damit zu exponentiell großer Verzögerung (im Durchmesser und der Knotenzahl des Netzwerks) gezwungen werden. Dies war bisher nur für konkrete prominente Strategien bekannt. * Es wird eine neue Technik zur Feststellung der Stabilität von Queueing Strategien ohne Zeitnahme vorgestellt, die Aufschichtungskreise. Mit ihrer Hilfe können bekannte Stabilitätsbeweise prominenter Strategien vereinheitlicht werden und weitere Stabilitätsergebnisse erzielt werden. * Für die große Teilklasse distanzbasierter Queueing Strategien gelingt eine vollständige Klassifizierung aller 1-stabilen und universell stabilen Strategien.
Es steht ausser Zweifel, das der Schutz der Privatsphäre von Internet-Nutzern gegenwärtig unzureichend ist. Die Chance sich im Netz relativ weiträumig und frei zu bewegen, steht die Möglichkeit gegenüber allerlei Informationen über Internet-Nutzer zu sammeln und auszuwerten. Dies ist natürlich auch im Intranet möglich. Im Rahmen dieser Diplomarbeit wurden die verschiedenen Möglichkeiten überprüft, die zur Veröffentlichung von Datenschutzmassnahmen angeboten werden. Zunächst ist der OECD Privacy Statement Generator, dessen Principles Grundlage bei der Formulierung von Lufthansa Principles waren, auf Lufthansatauglichkeit untersucht worden. Dabei hat sich ergeben, dass trotz der theoretischen Übereinstimmung der Principles der Lufthansa AG mit denen der OECD, der Gebrauch des Generators bei Lufthansa in dieser Form nicht möglich ist. Da anfänglich eine Anpassung des Generators an Lufthansabedürfnisse geplant war, sind im Rahmen dieser Diplomarbeit Änderungsvorschläge gemacht worden. Die Anpassung des Codes erfolgte nicht, da dieser nur für öffentliche Stellen und nicht für Privatunternehmen zugänglich ist. Mit P3P entwickelte das W3C eine Datenschutztechnik, die für Nutzer die Kontrolle über persönliche Daten automatisiert und damit den Schutz der Privatsphäre und die Akzeptanz der User verbessert. Nach der Einführung des P3P- und APPEL-Vokabulars, mit dem man einerseits Datenschutzmassnahmen und andererseits Datenschutzpräferenzen ausdrücken kann, sollte daher geprüft werden, ob dieses Vokabular ausreicht, um Lufthansa-spezifische Aussagen zu machen und in wieweit diese erweiterbar bzw. anpassbar sind. Die Untersuchung hat ergeben, dass das Vokabular bis zu einem gewissen Masse ausreicht und es ein Element gibt, das EXTENSION Element, mit dem eine Erweiterung des P3P Standardvokabulars möglich ist. Im Rahmen dieser Arbeit wurden solche auf Lufthansa abgestimmte Erweiterungen sowohl für eine P3P Policy als auch für eine entsprechende APPEL Präferenz formuliert. Die Lufthansa AG hat somit mit P3P die Möglichkeit, Ihre Datenschutzpraktiken für den Mitarbeiter transparenter zu gestalten, da sie auch über das Standardvokabular hinausgehende Aussagen formulieren kann. In der Diplomarbeit sind ausserdem die sich zur Zeit auf dem Markt befindlichen Tools, die bei der Erstellung einer maschinenlesbaren Datenschutzmassnahme, der sog. Privacy Policy benutzt werden können, untersucht worden. Der IBM P3P Policy Editor scheint für den Gebrauch bei Lufthansa denkbar, da die Handhabung des Generators einfach ist. Der Mitarbeiter, der die Policy für seine Abteilung erstellen soll, braucht sich nicht mit den Einzelheiten des P3P Vokabulars auseinander setzten. Mit diesem Editor kann zunächst ein Basisgerüst einer Policy erstellt werden. Die mit dem P3P Element EXTENSION formulierten Erweiterungen müssen jedoch selbsterstellt werden und können nachträglich in das Basisgerüst der Policy miteingebunden werden. Zusätzlich zu der maschinenlesbaren Form einer Policy erstellt der IBM Editor auch eine menschenlesbare HTML-Version der Policy. Dies ist sehr von Vorteil, da in einem Arbeitsgang zwei Policy-Versionen erstellt werden. Im Vergleich zu dem Formulierungsentwurf des OECD Generators ist die menschenlesbare Version des IBM Editors ausserdem wesentlich kürzer und dadurch auch übersichtlicher. Im Ganzen ist es daher sinnvoller, den IBM Editor zu benutzen, als den OECD Generator neu zu programmieren und dann mit Hilfe eines anderen Tools die P3P Policy zu erstellen. Zur Erstellung einer APPEL Präferenz ist zur Zeit nur ein Hilfsmittel auf dem Markt erhältlich. Der Grund hierfür ist sicherlich, dass sich APPEL noch zu keinem Standard entwickelt hat, sondern sich noch in einem Entwurfsstadium befindet. Der APPEL Editor von JRC ist ähnlich wie der P3P Policy Editor von IBM aufgebaut. Auch hier müssen Erweiterungen selbst formuliert und in dem vom Editor erstellten Basisgerüst einer Präferenz eingebunden werden. Nachdem die grundsätzliche Erweiterbarkeit von P3P in dieser Diplomarbeit festgestellt wurde, sind die sog. User Agents behandelt worden. Von Bedeutung war neben der Funktionsweise der einzelnen User Agents ihre Handhabung des EXTENSION Elementes. Da zu erwarten ist, dass nur wenige Nutzer die Voreinstellungen ihrer Software selbst verändern und sich mit der APPEL Spezifikation auseinander setzten, wird der Standardkonfiguration eines P3P User Agents eine große Bedeutung beigemessen. Bei allen vorgestellten User Agents gab es verschiedene Sicherheitsniveaux bzgl. Datenschutz aus denen der Nutzer auswählen konnte. Entsprechend des Niveaux wurde die Präferenz des Nutzers automatisch konfiguriert. Bei allen war es ausserdem möglich, selbsterstellte APPEL Formulierungen zu importieren. Bei dem Proxy von JRC ist es möglich, Settings mit einzubinden, die das EXTENSION Element beinhalten. AT&T erlaubt dies nicht und von Microsoft fehlt hierzu jegliche Angabe. Bzgl. der Lufthansa AG erscheint es sinnvoll, den Mitarbeitern einen eigenen User Agent anzubieten, der alle zusätzlich formulierten Aspekte aufgreift und mit dem der Mitarbeiter seine Präferenzen bzgl. des Intranets leicht ausdrücken kann. Der Aufwand, den Mitarbeitern das erweiterte Vokabular für die Formulierung einer Präferenz zur Verfügung zu stellen, setzt voraus, dass jeder Mitarbeiter sich mit der Syntax und Semantik von P3P und APPEL auskennt. Dies ist im Vergleich zur Programmierung eines eigenen User Agents, der den Mitarbeitern zur Verfügung gestellt wird, aufwendiger und wahrscheinlich auch nicht realisierbar. Grundsätzlich kann durch diese Massnahmen das Vertrauen der Mitarbeiter ins Intranet und damit die Nutzung dieses Mediums gesteigert werden. Die vermehrte Nutzung des Intranets auch für private Zwecke, wie zum Beispiel der Buchung von Reisen oder die Abfrage nach Flügen etc., würde für beide Seiten auch wirtschaftlichen Nutzen bringen. Für die Mitarbeiter selbst käme es z.B. zu einer Zeitersparnis, da sie jetzt zur Buchung ihrer Reisen nicht mehr in die Reisestelle müssen. Dies hätte natürlich auch wirtschaftliche Auswirkungen, da der Aufwand, um zur Reisestelle zu kommen, wegfällt. Aber auch die Lufthansa AG hätte durch die transparentere Gestaltung ihrer Datenschutzpraktiken wirtschaftlichen Nutzen. Die Mitarbeiter z.B. in der Reisestelle würden durch das neue Vertrauen ihrer Kollegen ins Intranet und damit einhergehend die selbstständige Online-Buchungsmöglichkeit entlastet werden. Es könnten mehr Kapazitäten für andere Aufgaben frei werden. Das Ausmass der Vorteile für Lufthansa und Ihrer Mitarbeiter, die sich aus der Veröffentlichung von Datenschutzmaßnahmen ergeben und damit ist auch das vermehrte Vertrauen der Mitarbeiter ins Intranet gemeint, ist zur Zeit noch nicht in vollem Umfang erfassbar, da sich viele Intranetprojekte der Lufthansa AG noch im Entwicklungsstadium befinden. Für die Zukunft ist jedoch auch festzustellen, dass datenschutzfreundliche Technologien allein nicht die Lösung zur Sicherstellung des Datenschutzes im Inter- als auch im Intranet sein können. Vielmehr müssen die aufkommenden technischen Maßnahmen durch nationale und internationale Regelungen unterstützt und ergänzt werden. Erst durch Festlegung internationaler Konventionen, die den Datenschutz in Zusammenhang mit grenzüberschreitenden Computernetzwerken und Diensten regeln, kann ein effektiver und unabhängiger Kontrollmechanismus sowie die Möglichkeit zu Sanktionen gewährleistet werden. Die Veröffentlichung von Datenschutzmassnahmen gewährleistet leider nicht ihre Einhaltung.
Sharing of substructures like subterms and subcontexts in terms is a common method for space-efficient representation of terms, which allows for example to represent exponentially large terms in polynomial space, or to represent terms with iterated substructures in a compact form. We present singleton tree grammars as a general formalism for the treatment of sharing in terms. Singleton tree grammars (STG) are recursion-free context-free tree grammars without alternatives for non-terminals and at most unary second-order nonterminals. STGs generalize Plandowski's singleton context free grammars to terms (trees). We show that the test, whether two different nonterminals in an STG generate the same term can be done in polynomial time, which implies that the equality test of terms with shared terms and contexts, where composition of contexts is permitted, can be done in polynomial time in the size of the representation. This will allow polynomial-time algorithms for terms exploiting sharing. We hope that this technique will lead to improved upper complexity bounds for variants of second order unification algorithms, in particular for variants of context unification and bounded second order unification.
In dieser Arbeit definieren wir ein Maß für den Grad der Mehrdeutigkeit (degree of ambiguity da) kontextfreier Grammatiken und Sprachen als die Anzahl der Ableitungsbäume in Abhängigkeit von der Länge n eines Wortes. Wir zeigen, dass es weder Sprachen noch zyklenfreie Grammatiken gibt, deren Mehrdeutigkeitsgrad stärker als 2£(n) wächst (wie z B. £(nn)). Aus [10] ist es außerdem bekannt, dass es keine Grammatiken (und somit keine Sprachen) gibt, deren Mehrdeutigkeit stärker als polynomiell, aber schwächer als exponentiell wächst (wie z. B. £(2pn). Deshalb untersuchen wir in dieser Arbeit hauptsächlich konstant mehrdeutige, polynomiell mehrdeutige und exponentiell mehrdeutige Grammatiken und Sprachen. Für jede feste, ganze Zahl k 2 N hat Maurer [8] die Existenz einer k-deutigen kontextfreien Sprache nachgewiesen. Durch Verwendung einer einfacheren Sprache, nämlich der Sprache Lk := fambm1 1 bm2 2 : : : bmk k jm;m1;m2; : : : ;mk ¸ 1; 9 i mit m = mig, und mit Hilfe von Ogden's Lemma1 erhalten wir einen wesentlich kürzeren Beweis. Ferner zeigen wir die Existenz exponentiell mehrdeutiger Sprachen. Wir zeigen, dass die Sprache L¤ { wobei L = faibicj ji; j ¸ 1g [ faibjciji; j ¸ 1g-exponentiell mehrdeutig ist, indem wir beweisen, dass das Wort (ah+h!bh+h!ch+h!)k mindestens 2k Ableitungen in jeder Grammatik G für L¤ hat, wobei k aus N ist und h die Konstante aus Ogden's Lemma für G ist. Für beliebig kleines c aus R+ entwerfen wir eine Grammatik Gc für L¤, so dass daGc · 2cn gilt. Somit gilt, dass die Sprache L¤ zwar exponentiell mehrdeutig ist, aber es gibt kein festes c aus R+ , so dass L¤ 2cn-deutig ist. Wir geben polynomiell mehrdeutige Grammatiken an und zeigen die Existenz von polynomiell mehrdeutigen Sprachen, indem wir mit Hilfe von Ogden's Lemma beweisen, dass die Anzahl der Ableitungsbäume eines Wortes der Länge n in jeder Grammatik für die Sprache Lk in der Größenordnung von (nk) liegt, wobei k eine Konstante aus N ist, und L := fambm1cbm2c : : : bmpcjp 2 N; m;m1;m2; : : : ;mp 2 N; 9i 2 f1; 2; : : : ; pg mit m = mig gilt. Durch Angabe einer O(nk){deutigen Grammatik zeigen wir schließlich, dass Lk polynomiell vom Grad k mehrdeutig ist. Außerdem entwerfen wir für jedes feste d aus R+ eine Grammatik Gd für L, so dass daGd · dn dn für genügend großes n ist.
Considered are the classes QL (quasilinear) and NQL (nondet quasllmear) of all those problems that can be solved by deterministic (nondetermlnlsttc, respectively) Turmg machines in time O(n(log n) ~) for some k Effloent algorithms have time bounds of th~s type, it is argued. Many of the "exhausUve search" type problems such as satlsflablhty and colorabdlty are complete in NQL with respect to reductions that take O(n(log n) k) steps This lmphes that QL = NQL iff satisfiabdlty is m QL CR CATEGORIES: 5.25
Das Thema dieser Arbeit ist die Dienstvermittlung in offenen verteilten Systemen und die Rolle, die ein Typsystem dabei einnimmt. Ein Typsystem besteht aus einer Typbeschreibungssprache und der Definition einer Typkonformität. Die Typbeschreibungssprache erlaubt die Spezifiation von Typen, wohingegen mit der Typkonformität während eines Vermittlungsvorgangs überprüft wird, ob Angebot und Nachfrage zusammenpassen. In dieser Arbeit wurde zunächst nachgewiesen, daß es sinnvoll ist, bei einem Typ zwischen seiner Intension und seiner Extension zu unterscheiden. Die Intension eines Typs ist die Gesamtheit aller Beschreibungen, die auf diesen zutreffen. Die Extension eines Typs repräsentiert dagegen eine konkrete Beschreibung (d.h. Spezifikation eines Dienstangebots). Eine Interpretation ordnet jeder Extension eine Intension zu. Um in einem offenen verteilten System Dienste vermitteln zu können, müssen sich Dienstnutzer und {anbieter auf die Extensionen aller Typen einigen. Einem Typ kommt hierdurch die Rolle eine Standards zu, der allen beteiligten Parteien a priori bekannt sein muß. Daraus resultiert eine injektive Interpretation, die jeder Intension genau eine Extension zuordnet. Die eindeutig bestimmte Extension einer Intension fungiert als systemweiter Standard. Ein Typ als Standard steht im Widerspruch zu der Vielfalt und Dynamik eines offenen Dienstmarktes. Der Standardisierungsprozeß von Extensionen, der einem Vermittlungsvorgang vorausgehen muß, hemmt gerade die Dynamik des Systems. Die Konsequenz daraus ist, daß neben den Diensten auch die Diensttypen Gegenstand der Vermittlung sein müssen. Diese Schlußfolgerung ist bisher noch nicht formuliert worden. Es wäre somit wünscheswert, nicht{injektive Interpretationen zuzulassen, so daß eine Intension mehrere Extensionen besitzen kann, die unterschiedliche Sichten der Dienstnutzer und {anbieter repräsentieren. Die Analyse einiger bestehender Typsysteme zeigte, daß mit diesen eine nicht-injektive Interpretation nicht realisierbar ist. Im Hauptteil dieser Arbeit wurden zwei neue Typsysteme vorgestellt, die diese Eigenschaft unterstützen. Das deklarative Typsystem erweitert die Schnittstellenbeschreibungssprache eines syntaktischen Typsystems, indem semantische Spezifiationen zugelassen werden. Die deklarative Semantik dient dabei als Grundlage für die Beschreibung der Semantik einer Typspezifikation. Die Extension entspricht einem definiten Programm bestehend aus einer endlichen Menge von Horn-Klauseln. Die Intension eines Typs korrespondiert mit dem kleinsten Herbrand-Modell des definiten Programms, welches die semantische Spezifikation des Typs darstellt. Die Forderung nach der Möglichkeit nicht{injektiver Interpretationen ergibt sich aus den Eigenschaften der deklarativen Semantik, wonach verschiedene definite Programme ein identisches kleinstes Herbrand-Modell besitzen können. Das zweite in dieser Arbeit vorgestellte Typsystem entspringt einem wissensbasierten Ansatz. Grundlage bildet eine Wissensrepräsentationstechnik, die anwenderbezogene semantische Spezifikationen erlaubt. Ein Konzeptgraph als wissensbasierte Typspezifikation vereinigt in sich unterschiedliche Beschreibungen eines Typs. Ein Konzeptgraph, der selbst eine Extension darstellt, repräsentiert somit die Vereinigung mehrerer Extensionen eines Typs. Die Intension ist jedoch durch einen Konzeptgraph nicht eindeutig bestimmt. Dieser stellt lediglich eine Approximation dar. Hier liegt ein fundamentaler Unterschied in den beiden Typsystemen. Während eine Extension im deklarativen Typsystem auch immer eindeutig eine Intension charakterisiert, ist dies bei dem wissensbasierten Typsystem nicht der Fall. Die Konsequenz daraus ist, daß dieser Umstand bei einem Vermittlungsvorgang berücksichtigt werden muß. Ein wissensbasierter Vermittler muß über ein spezielles Vermittlungsprotokoll die Verfeinerung einer wissensbasierten Typspezifikation erlauben, die zu einer besseren Approximation der Intension führt. Das deklarative Typsystem besitzt aufgrund der Unentscheidbarkeit der deklarativen Typkonformität keine praktische Relevanz. Es zeigt jedoch, wie mit Hilfe der deklarativen Semantik der Open World Assumption genüge geleistet werden kann. Im Vergleich dazu kann das wissensbasierte Typsystem als "Fuzzyfizierung" des deklarativen Typsystems angesehen werden. Die wissensbasierte Typbeschreibungssprache ermöglicht im Sinne der Fuzzy Logik unscharfe Spezifikationen, die im Laufe der Zeit verfeinert werden. Ein Vorteil des wissensbasierten Ansatzes ist die Möglichkeit von anwenderbezogenen Typspezifikationen. Ein anderer Vorteil besteht darin, daß eine wissensbasierte Typbeschreibungssprache eine Meta-Sprache repräsentiert, in der Spezifikationen aus anderen Domänen dargestellt werden können. Ungeachtet dieser Vorteile bleibt jedoch der Beweis offen, daß die wissensbasierte Dienstvermittlung tatsächlich eine geeignete Methodik für die Vermittlung von Typen darstellt.
In this paper we present a non-deterministic call-by-need (untyped) lambda calculus lambda nd with a constant choice and a let-syntax that models sharing. Our main result is that lambda nd has the nice operational properties of the standard lambda calculus: confluence on sets of expressions, and normal order reduction is sufficient to reach head normal form. Using a strong contextual equivalence we show correctness of several program transformations. In particular of lambdalifting using deterministic maximal free expressions. These results show that lambda nd is a new and also natural combination of non-determinism and lambda-calculus, which has a lot of opportunities for parallel evaluation. An intended application of lambda nd is as a foundation for compiling lazy functional programming languages with I/O based on direct calls. The set of correct program transformations can be rigorously distinguished from non-correct ones. All program transformations are permitted with the slight exception that for transformations like common subexpression elimination and lambda-lifting with maximal free expressions the involved subexpressions have to be deterministic ones.
Entwurf und Realisierung von Sicherheitsmechanismen für eine Infrastruktur für digitale Bibliotheken
(2002)
Angesichts der überragenden Bedeutung der modernen Kommunikationstechnik in allen Lebensbereichen kommt auch den digitalen Bibliotheken ein wachsendes Gewicht zu. Dabei spielen nicht nur die platzsparende Speicherung, sondern auch die schnelle Datenübermittlung und der unmittelbare Zugang zu den Dokumenten eine wichtige Rolle. Da eine solche Bibliothek über ein offenes Netz betrieben wird, erhalten in diesem Zusammenhang Sicherheitsaspekte ein essentielles Gewicht. Die vorliegende Diplomarbeit geht diesen Fragen nach und zeigt Wege auf, wie die bestehenden Sicherheitsrisiken minimiert werden können. Ziel dieser Arbeit war daher der Entwurf und die Realisierung von Sicherheitsmechanismen für eine Infrastruktur für digitale Bibliotheken. Dabei wurde speziell auf die INDIGO-Infrastruktur eingegangen; sie stellt eine verteilte Infrastruktur für digitale Bibliotheken dar. Der erste Teil dieser Diplomarbeit enthält eine Einführung in die Grundlagen der INDIGO-Infrastruktur und der Sicherheit. In Kapitel [*] wurden die INDIGO-Infrastruktur und ihre Komponenten erläutert; in Kapitel [*] folgte anschließend die Beschreibung einiger kryptographischer Verfahren und Sicherheitsprotokolle. Im zweiten Teil dieser Arbeit wurden Sicherheitsmechanismen für die INDIGO-Infrastruktur entworfen. In dieser Entwurfsphase erfolgte zunächst in Kapitel [*] die Sicherheitsanalyse der Infrastruktur. Basierend auf dieser Analyse wurden in Kapitel [*] Sicherheitskonzepte für diese Infrastruktur entwickelt. Während der gesamten Entwurfsphase standen die Sicherheitsanforderungen Vertraulichkeit, Authentizität, Integrität, Verbindlichkeit und die Autorität stets im Mittelpunkt des Interesses. Im dritten und letzten Teil der Arbeit wurden die Sicherheitsmechanismen für die INDIGO-Infrastruktur realisiert. Dabei wurden die in Abschnitt [*] beschriebenen Sicherheitsrichtlinien der Infrastruktur implementiert. Die Beschreibung der Implementierung erfolgte in Kapitel [*]. Die wichtigsten Modifikationen des INDIGO-Servers betrafen folgende Punkte: * Sicherung und Aufbau der verbindlichen Kommunikationskanäle durch den Einsatz von SSL- bzw. TLS-basierten Server-zu-Server Verfahren. * Realisierung von Sicherheitsmechanismen zur Verifikation der digital signierten Dokumente und Dokumentmethoden. * Erweiterung des INDIGO-Servers um feingranuliert konfigurierbare Zugriffsmechanismen, die verteilt auf drei unterschiedliche Ebenen den Zugriff der Anwender (bzw. Dokumentmethoden) auf seine Ressourcen kontrollieren. Neben den Modifikationen des INDIGO-Servers wurden zwei neue Clients zur Kommunikation mit dem INDIGO-Server und eine Anwendung zur Erzeugung der digitalen Signatur der Dokumente entwickelt. Ferner wurden einige neue Metadokumente und Dokumentmethoden erstellt, um die neuen Eigenschaften der Infrastruktur zu demonstrieren. Bei der Realisierung der Sicherheitsmechanismen wurde größter Wert auf die Abwärtskompatibilität, Konfigurierbarkeit und Modularität gelegt. Die Abwärtskompatibilität zur ursprünglichen Infrastruktur wird beispielsweise erreicht, indem die bereits existierenden Metadokumente und Dokumentmethoden bei dem modifizierten Server auch verwendet werden können. Diese müssen - falls nötig - minimal um die digitale Signatur der Autoren ergänzt werden. Das Sicherheitsverhalten des INDIGO-Servers läßt sich beliebig über seine Konfigurationsdatei ändern (Konfigurierbarkeit). Alle wichtigen Sicherheitsmechanismen des modifizierten Servers lassen sich den Wünschen des Betreibers anpassen. Dadurch ist sichergestellt, daß jeder Betreiber den Server seinen jeweiligen Sicherheitsbedürfnissen entsprechend betreiben kann. Der Betreiber kann beispielsweise über die Einstellung seiner Konfigurationsdatei bestimmen, ob die Clients sich bei der Kommunikation mit seinem Server identifizieren müssen. Zudem kann er beispielsweise festlegen, ob die Dokumentmethoden, die keine korrekte digitale Signatur besitzen, ausgeführt werden dürfen oder nicht. Die Konfigurierbarkeit des Servers hinsichtlich der Sicherheitsmechanismen geht sogar so weit, daß man den Server im Normalmodus betreiben kann; in diesem Modus sind alle Sicherheitsmechanismen des Servers ausgeschaltet. Die Modularität hinsichlich der Sicherheitsmechanismen wurde bei der Implementierung durch die Verteilung dieser Mechanismen auf die unterschiedlichen und eigenständigen Klassen erzielt, die jeweils eine wohldefinierte Eigenschaft und Aufgabe besitzen. Diese Vorgehensweise führt dazu, daß bei einer Weiterentwicklung des Servers um neue Sicherheitsdienste nur die wenigen betroffenen Klassen modifiziert werden müssen, ohne daß der gesamte Server davon betroffen ist. So kann der INDIGO-Server beispielsweise um den Authentisierungsdienst Kerberos [Stei88] erweitert werden, in dem nur die entsprechende Authentisierungsklasse des Servers (IndigoAuthorization-Klasse) ergänzt wird.
Visualisierungssysteme nutzen die Mittel der modernen Computergraphik, um Informationen und Zusammenhänge zu veranschaulichen. Ein wichtiges Teilgebiet besteht dabei in der Veranschaulichung großer Informationsmengen zur Gewinnung eines Überblicks und Vorauswahl potentiell interessanter Teilmengen, die dann mit weiterführenden Methoden im Detail erforscht werden können. Das Relevanzkugelmodell wurde erstmals eingeführt, um als Bestandteil des LyberWorld-Projekts genau diese Vorselektion auf einer Menge von Textdokumenten zu leisten. Ziel dieser Arbeit ist es, dieses Modell in eine neue Form auf Basis des World Wide Web zu überführen und damit aus der engen Anbindung an das ursprüngliche System zu lösen und allgemeiner verwendbar zu machen. Zu diesem Zweck werden zunächst das Modell an sich und seine früheren Implementierungen genauer betrachtet, dann nach Auswahl geeigneter Hilfsmittel – VRML zur graphischen Modellierung und Java zur Handhabung der Funktionalität – Konzepte zur weiteren Ausgestaltung und zur Behebung existierender Schwächen des Ansatzes erarbeitet, und schließlich die resultierende Implementierung beschrieben und bewertet.
We study the approximability of the following NP-complete (in their feasibility recognition forms) number theoretic optimization problems: 1. Given n numbers a1 ; : : : ; an 2 Z, find a minimum gcd set for a1 ; : : : ; an , i.e., a subset S fa1 ; : : : ; ang with minimum cardinality satisfying gcd(S) = gcd(a1 ; : : : ; an ). 2. Given n numbers a1 ; : : : ; an 2 Z, find a 1-minimum gcd multiplier for a1 ; : : : ; an , i.e., a vector x 2 Z n with minimum max 1in jx i j satisfying P n...
Configuration, simulation and visualization of simple biochemical reaction-diffusion systems in 3D
(2004)
Background In biological systems, molecules of different species diffuse within the reaction compartments and interact with each other, ultimately giving rise to such complex structures like living cells. In order to investigate the formation of subcellular structures and patterns (e.g. signal transduction) or spatial effects in metabolic processes, it would be helpful to use simulations of such reaction-diffusion systems. Pattern formation has been extensively studied in two dimensions. However, the extension to three-dimensional reaction-diffusion systems poses some challenges to the visualization of the processes being simulated. Scope of the Thesis The aim of this thesis is the specification and development of algorithms and methods for the three-dimensional configuration, simulation and visualization of biochemical reaction-diffusion systems consisting of a small number of molecules and reactions. After an initial review of existing literature about 2D/3D reaction-diffusion systems, a 3D simulation algorithm (PDE solver), based on an existing 2D-simulation algorithm for reaction-diffusion systems written by Prof. Herbert Sauro, has to be developed. In a succeeding step, this algorithm has to be optimized for high performance. A prototypic 3D configuration tool for the initial state of the system has to be developed. This basic tool should enable the user to define and store the location of molecules, membranes and channels within the reaction space of user-defined size. A suitable data structure has to be defined for the representation of the reaction space. The main focus of this thesis is the specification and prototypic implementation of a suitable reaction space visualization component for the display of the simulation results. In particular, the possibility of 3D visualization during course of the simulation has to be investigated. During the development phase, the quality and usability of the visualizations has to be evaluated in user tests. The simulation, configuration and visualization prototypes should be compliant with the Systems Biology Workbench to ensure compatibility with software from other authors. The thesis is carried out in close cooperation with Prof. Herbert Sauro at the Keck Graduate Institute, Claremont, CA, USA. Due to this international cooperation the thesis will be written in English.
Die Leistungsfähigkeit moderner Grafikhardware erreicht ein Niveau, auf dem sich selbst aufwändig gestaltete 3D-Szenen in kürzester Zeit berechnen lassen. Die Möglichkeiten, die diese Systeme zur Navigation und Interaktion im dreidimensionalen Raum bieten, erscheinen vielen Anwendern jedoch nicht intuitiv genug. Das Ziel der vorliegenden Arbeit war es, neue Navigations- und Interaktionstechniken für räumliche Anwendungen zu entwerfen und anhand einer prototypischen Implementierung die Eignung dieser Techniken für die Interaktion mit einem virtuellen Modell des Rubik’s Cube zu untersuchen. Da die entwickelten Verfahren ihre Tauglichkeit insbesondere bei der Interaktion über klassische Ein- und Ausgabegeräte unter Beweis stellen sollten (Maus, Tastatur und 2D-Display), waren geeignete Abbildungen der zu beherrschenden Freiheitsgrade zu konzipieren. Die Beschreibung grundlegender Aspekte der menschlichen Wahrnehmung führte zum Konzept der 3D-Metapher, welche die Durchführung einer dreidimensionalen Operation mit Hilfe von 2D-Eingabegeräten erklärt. Einzelne Interaktionsaufgaben des 3D-Raums wurden dargestellt und Beispiele von metaphorischen Konzepten für ihre Implementierung gegeben. Nach der Darstellung der am Rubik’s Cube auftretenden Interaktionsformen wurden metaphorische Konzepte für die Operationen Inspektion und Rotation entworfen und ihre besonderen Eigenschaften beschrieben; hierbei wurde zudem auf spezielle Verfahren eingegangen, die bei der Implementierung dieser Metaphern eingesetzt wurden. Im Rahmen einer Benutzerstudie wurde die Bedienung der konzipierten Interaktionsmetaphern im praktischen Einsatz getestet. Hierbei wurden insbesondere die Kriterien Intuitivität, Effizienz und Erlernbarkeit untersucht sowie die zeitliche Performance und Fehlerhäufigkeiten beim Einsatz der unterschiedlichen Werkzeuge analysiert. Die vorliegende Arbeit bietet eine Reihe von Ansätzen für künftige Erweiterungen, wie zum Beispiel die Weiterentwicklung zu einer Autorenumgebung für interaktive Anwendungen oder die Integration eines Kommunikationskanals zwischen den einzelnen Interaktionsmetaphern, um auf diese Weise auch komplexe Verhaltensmuster implementieren zu können.
Grafik-Hardware ist programmierbar geworden. Graphic Processing Units (GPUs) der neuen Generation wie der GeForce3 von NVIDIA enthalten Prozessoren, die es dem Software-Entwickler erlauben kurze Routinen auf der Grafik-Hardware auszuführen. Ich gebe in dieser Arbeit einen umfassenden Überblick über die Architekur und Leistungsfähigkeit dieser neuen Chipgeneration, zeige deren Stärken und Schwächen auf und diskutiere Verbesserungsvorschläge. Als Teil der Arbeit präsentiere ich einige von mir entwickelte Schattierungsverfahren, sowie eine Wassersimulation. Diese Demonstratoren sind darauf ausgerichtet vollständig auf den Prozessoren der neuen Grafikchip- Generation zu laufen. Als Antwort auf die Mängel der zur Zeit verfügbaren Application Programming Interfaces stelle ich ein alternatives Interface zur Steuerung der neuen GPUKomponenten vor, das insbesondere die Austauschbarkeit und Kombinierbarkeit von GPU-Programmen unterstützt.
Immer mehr Hersteller bringen kleine mobile Endgeräte (PDAs1) auf den Markt, die via WLAN2 (IEEE 802.11), Bluetooth oder UMTS3 drahtlos Kontakt mit der Außenwelt aufnehmen können. Dabei werden neben zunehmend höheren Übertragungsraten auch große Fortschritte in der Miniaturisierung erzielt. Viele PDAs besitzen bereits eingebaute Funknetzwerk-Karten, bei vielen läßt sich eine solche Karte einfach zusätzlich in das Gerät einstecken. Durch die steigende Rechenleistung der Geräte und die gleichzeitig steigenden Übertragungsraten der Funkverbindungen entstehen diverse neue Anwendungsmöglichkeiten, die allerdings noch wenig ausgenutzt werden. Es überwiegen die Standardaufgaben der PDAs, wie die Termin und die Adressenverwaltung. Ein eventuell vorhandener Zugang zu Netzwerken wird meist ebenfalls nur für Standardanwendungen verwendet, wie z.B. die Synchronisation von Daten mit einem Server, der Zugang zum World Wide Web oder zum Versenden von e-Mails. Der herkömmliche Zugang zu Netzwerken ist meist ortsgebunden. Im sogenannten Infrastruktur-Modus ist man auf eine Basisstation (Access-Point) angewiesen. Bewegt man sich in Bereichen, in denen kein solcher Access-Point zur Verfügung steht, kann eine Netzwerkverbindung nicht hergestellt werden. Die Mobilität des Benutzers ist auf die Funkreichweite seines Geräts zu dieser Basisstation beschränkt. Die Bezeichnung „mobil“ trifft also nur auf das Endgerät, nicht auf die Basisstation zu. Genutzt werden üblicherweise die gleichen Dienste wie in einem kabelgebundenem Netz, nämlich Server des Intra-, bzw. Internets. Die eigenständige Vernetzung mobiler Geräte untereinander, der sogenannte Ad-hoc-Modus, eröffnet neuartige Anwendungsgebiete. Ursprünglich dafür gedacht, zwei Stationen schnell und einfach über Funk miteinander zu verbinden, können durch eine Erweiterung beliebig viele Stationen zu einem spontanen und mobilen Netzwerk zusammengefaßt werden (mobiles Ad-hoc Netzwerk, MANET). Eine zentral verwaltete Infrastruktur entfällt dabei vollständig. Die Aufgaben des Routings muß jede einzelne der beteiligten Stationen übernehmen. Auf diese Weise erhöht sich die Funkreichweite aller beteiligten Stationen, da nicht ein zentraler Access-Point, sondern jeder beliebige Teilnehmer in Reichweite den Zugriff auf das Netzwerk ermöglicht. Es muß dabei allerdings davon ausgegangen werden, daß sich die Stationen in einem solchen Netz ständig bewegen, das Netz verlassen oder neu hinzukommen können. Somit verändert sich andauernd die Netzwerktopologie und ein kontinuierliches und selbstständiges Neuorganisieren des Netzes wird notwendig. Man spricht daher von selbstorganisierenden mobilen Netzen. Der Informationsfluß in Ad-hoc Netzen ist üblicherweise ein anderer als in Festnetzen. Es entsteht eine eher interessensbezogene Kommunikation, weniger eine, die auf dem Wissen von bekannten Endpunkten im Netzwerk basiert. In Ad-hoc Netzwerken können Endpunkte und Adressen aufgrund der sich permanent ändernden Nutzerzusammensetzung naturgemäß nicht bekannt sein. Stattdessen gibt jeder Nutzer Informationen über seine Interessen und seine Angebote im Netzwerk bekannt. Findet sich ein zu diesem Interessensprofil passendes Angebot, so kommt eine Verbindung zustande. Die Flexibilität der PDAs, ihre Mobilität und ihre ständig steigende Leistung lassen die Entwicklung von mobilen Ad-hoc-Anwendungen sinnvoll erscheinen. MANET Netzwerke sind in ihrer Auslegung flexibel und schnell, genau so, wie es die modernen PDAs sind. Es eröffnet sich durch durch beides eine große Zahl neuer und innovativer Anwendungsmöglichkeiten. Eine davon, das so genannte E-Learning, soll im Folgenden näher betrachtet werden. E-Learning ist ein Beispiel für eine Anwendung in Ad-hoc Netzen, die besonders geeignet erscheint, die Beweglichkeit ihrer Anwender in vielerlei Hinsicht zu unterstützen. Durch die Eigenschaft, geeignete Kollaborationspartner und Informationen schnell und gezielt im Netzwerk finden zu können, wird ein spontaner Wissensaustausch über die bisher bestehende Grenzen hinaus möglich. Es werden im Rahmen dieser Diplomarbeit Mechanismen behandelt, die dem Anwender die Nutzung von kollaborativen Anwendungen wie dem E-Learning ermöglichen und ihn bei dessen Nutzung unterstützen sollen.
Die Gitterbasenreduktion hat in der algorithmischen Zahlentheorie und der Kryptologie bedeutende und praktisch relevante Anwendungen [Joux und Stern, 1998; Nguyen und Stern, 2000; Nguyen, 2001]. Ein wesentlicher Beitrag auf dem Gebiet der Gitter-Reduktionsalgorithmen ist der LLL-Algorithmus [Lenstra, Lenstra und Lov´asz, 1982] und auch die Beta-Reduktion (BKZ-Reduktion) von Gitterbasen [Schnorr, 1987, 1988, 1994] ist von großer Bedeutung. Bei Implementierungen dieser Algorithmen auf modernen Rechnerarchitekturen erfolgen viele Berechnungen aus Gründen der schnelleren Verarbeitungsgeschwindigkeit in Gleitpunktzahlen-Arithmetik. Aufgrund inhärenter Rundungsfehler kommt es dabei zu numerischen Instabilitäten. Vor [Koy und Schnorr, 2001b] gab es keine erfolgreichen Ansätze die bei der Gitterbasenreduktion auftretenden Rundungsfehler so zu kontrollieren, dass auch Gitterbasen in der Dimension >= 400 reduziert werden können. Diese Diplomarbeit beschäftigt sich mit den praktischen Aspekten der Gitterbasenreduktion in Segmenten. Dabei handelt es sich um die erstmalige Implementierung und experimentelle Evaluierung der folgenden beiden Verfahren: ....
In den Anwendungsbereichen der Mixed Reality (MR) werden die reale und die virtuelle Welt kombiniert, so dass ein Eindruck der Koexistenz beider Welten entsteht. Meist wird dabei die reale Umgebung durch virtuelle Objekte angereichert, die dem Anwender zusätzliche Informationen bieten sollen. Um die virtuellen Objekte richtig zu positionieren, muss die reale Umgebung erkannt werden. Diese Erkennung der realen Umgebung wird meist durch Bestimmung und Verfolgung von Orientierung und Positionierung der realen Objekte realisiert, was als Tracking bezeichnet wird und einen der wichtigsten Bestandteile für MR-Anwendung darstellt. Ohne die exakte Ausrichtung von realen und virtuellen Objekten, geht die Illusion verloren, dass die virtuellen Objekte Teil der realen Umgebung sind und mit ihr verschmelzen. Markerkombination Das markerbasierte Tracking ist ein Verfahren, das die Bestimmung der Positionierung von realen Objekten durch zusätzliche Markierungen in der realen Umgebung ermöglicht. Diese Markierungen können besonders gut durch Bildanalyseverfahren extrahiert werden und bieten anhand ihrer speziellen Form Positionierungsinformationen. Der Einsatz dieser Trackingtechnologie ist dabei denkbar einfache und kostengünstig. Ein breiter Anwendungsbereich ist durch den kostengünstigen Einsatz dieser Technologien gegeben, allerdings ist das Erstellen von MR-Anwendungen fast ausschließlich MR-Spezialisten vorbehalten, die über Programmierfertigkeiten und spezielle Kenntnisse aus dem MR-Bereich besitzen. Diese Arbeit beschreibt die Entwicklung und Umsetzung der Konzepte, die einem Personenkreis, der lediglich über geringe Kenntnisse von MR-Technologien und deren Anwendung verfügt, den kostengünstigen und einfachen Einsatz von markerbasierten Trackingtechnologien ermöglicht. Die im Rahmen der Arbeit durchgeführte Analyse verweist auf die problematischen Anwendungsfälle des markerbasierten Trackings, die durch die Verdeckung von Markern zustande kommen, in der Beschränkung der Markeranzahl begründet sind, oder durch die Schwankung der Trackingangaben entstehen. Diese Problembereiche sind bei der Entwicklung berücksichtigt worden und können mit Hilfe der entwickelten Konzepte vom Autor bewältigt werden. Das Konzept der Markerkategorien ermöglicht dabei den Einsatz von angepassten Filterungstechniken. Die redundante Markerkombination behebt das Verdeckungsproblem und eliminiert Schwankungen durch das Kombinieren von mehreren Trackinginformationen. Die Gütefunktion ermöglicht die Bewertung von Trackinginformationen und wird zur Gewichtung der Trackingangaben innerhalb einer Markerkombination genutzt. Das Konzept der Markertupel ermöglicht eine Wiederverwendung von Markern, durch den Ansatz der Bereichsunterteilung. Die Konzepte sind in der AMIRE-Umgebung vollständig implementiert und getestet worden. Zum Abschluss ist rückblickend eine kritische Betrachtung der Arbeit, in punkto Vorgehensweise und erreichter Ergebnisse durchgeführt worden.
Die Anfänge der Gittertheorie reichen in das letzte Jahrhundert, wobei die wohl bekanntesten Ergebnisse auf Gauß, Hermite und Minkowski zurückgehen. Die Arbeiten sind jedoch zumeist in der Schreibweise der quadratischen Formen verfaßt, erst in den letzten Jahrzehnten hat sich die von uns verwendete Gitterschreibweise durchgesetzt. Diese ist zum einen geometrisch anschaulicher, zum anderen wurden in den letzten Jahren für diese Schreibweise effiziente Algorithmen entwickelt, so daß Probleme der Gittertheorie mittels Computer gelöst werden können. Ein wichtiges Problem ist, in einem Gitter einen kürzesten nicht verschwindenden Vektor zu bestimmen. Den Grundstein für diese algorithmische Entwicklung legten A.K. Lenstra, H.W. Lenstra Jr. und L. Lovasz mit ihrer Arbeit. In dieser führten sie einen Reduktionsbegriff ein, der durch einen Polynomialzeitalgorithmus erreicht werden kann. Ein weiterer Reduktionsbegriff, die Blockreduktion, geht auf Schnorr zurück. Euchner hat im Rahmen seiner Diplomarbeit effiziente Algorithmen für diese beiden Reduktionsbegriffe auf Workstations implementiert und auch in Dimensionen > 100 erfolgreich getestet. Die Verbesserungen von Schnittechniken des in der Blockreduktion verwendeten Aufzählungsverfahrens und die Einführung einer geschnittenen Aufzählung über die gesamte Gitterbasis hat Hörner in seiner Diplomarbeit beschrieben. Ziel der folgenden Arbeit war es nun, diese bereits auf sequentiellen Computern implementierten Algorithmen zu modifizieren, um auf parallelen Rechnern, speziell Vektorrechnern, einen möglichst hohen Geschwindigkeitsgewinn zu erzielen. Wie in den seriellen Algorithmen werden die Basisvektoren stets in exakter Darstellung mitgeführt, so daß das Endergebnis einer Berechnung nicht durch Rundungsfehler verfälscht wird.
Im Jahr 1993 schlug A. Shamir Protokolle zur Erstellung digitaler Unterschriften vor, die auf rationalen Funktionen kleinen Grades beruhen. D. Coppersmith, J. Stern und S. Vaudenay präsentierten die ersten Angriffe auf die Verfahren. Diese Angriffe können den geheimen Schlüssel nicht ermitteln. Für eine der von Shamir vorgeschlagenen Varianten zeigen wir, wie der geheime Schlüssel ermittelt werden kann. Das zweite Signaturschema von Shamir hängt von der Wahl einer algebraischen Basis ab. Eine besondere Bedeutung haben Basen, deren Elemente polynomiale Terme vom Grad 2 sind. Wir analysieren die Struktur der algebraischen Basen. Für den hervorgehobenen Spezialfall kann eine vollständige Klassifikation durchgeführt werden.
We introduce a new method for representing and solving a general class of non-preemptive resource-constrained project scheduling problems. The new approach is to represent scheduling problems as de- scriptions (activity terms) in a language called RSV, which allows nested expressions using pll, seq, and xor. The activity-terms of RSV are similar to concepts in a description logic. The language RSV generalizes previous approaches to scheduling with variants insofar as it permits xor's not only of atomic activities but also of arbitrary activity terms. A specific semantics that assigns their set of active schedules to activity terms shows correctness of a calculus normalizing activity terms RSV similar to propositional DNF-computation. Based on RSV, this paper describes a diagram-based algorithm for the RSV-problem which uses a scan-line principle. The scan-line principle is used for determining and resolving the occurring resource conflicts and leads to a nonredundant generation of all active schedules and thus to a computation of the optimal schedule.
In the last years, much effort went into the design of robust anaphor resolution algorithms. Many algorithms are based on antecedent filtering and preference strategies that are manually designed. Along a different line of research, corpus-based approaches have been investigated that employ machine-learning techniques for deriving strategies automatically. Since the knowledge-engineering effort for designing and optimizing the strategies is reduced, the latter approaches are considered particularly attractive. Since, however, the hand-coding of robust antecedent filtering strategies such as syntactic disjoint reference and agreement in person, number, and gender constitutes a once-for-all effort, the question arises whether at all they should be derived automatically. In this paper, it is investigated what might be gained by combining the best of two worlds: designing the universally valid antecedent filtering strategies manually, in a once-for-all fashion, and deriving the (potentially genre-specific) antecedent selection strategies automatically by applying machine-learning techniques. An anaphor resolution system ROSANA-ML, which follows this paradigm, is designed and implemented. Through a series of formal evaluations, it is shown that, while exhibiting additional advantages, ROSANAML reaches a performance level that compares with the performance of its manually designed ancestor ROSANA.
In the last decade, much effort went into the design of robust third-person pronominal anaphor resolution algorithms. Typical approaches are reported to achieve an accuracy of 60-85%. Recent research addresses the question of how to deal with the remaining difficult-toresolve anaphors. Lappin (2004) proposes a sequenced model of anaphor resolution according to which a cascade of processing modules employing knowledge and inferencing techniques of increasing complexity should be applied. The individual modules should only deal with and, hence, recognize the subset of anaphors for which they are competent. It will be shown that the problem of focusing on the competence cases is equivalent to the problem of giving precision precedence over recall. Three systems for high precision robust knowledge-poor anaphor resolution will be designed and compared: a ruleset-based approach, a salience threshold approach, and a machine-learning-based approach. According to corpus-based evaluation, there is no unique best approach. Which approach scores highest depends upon type of pronominal anaphor as well as upon text genre.
Assessing enhanced knowledge discovery systems (eKDSs) constitutes an intricate issue that is understood merely to a certain extent by now. Based upon an analysis of why it is difficult to formally evaluate eKDSs, it is argued for a change of perspective: eKDSs should be understood as intelligent tools for qualitative analysis that support, rather than substitute, the user in the exploration of the data; a qualitative gap will be identified as the main reason why the evaluation of enhanced knowledge discovery systems is difficult. In order to deal with this problem, the construction of a best practice model for eKDSs is advocated. Based on a brief recapitulation of similar work on spoken language dialogue systems, first steps towards achieving this goal are performed, and directions of future research are outlined.
Robuste Anaphernresolution
(2004)
In the last years, much effort went into the design of robust anaphor resolution algorithms. Many algorithms are based on antecedent filtering and preference strategies that are manually designed. Along a different line of research, corpus-based approaches have been investigated that employ machine-learning techniques for deriving strategies automatically. Since the knowledge-engineering effort for designing and optimizing the strategies is reduced, the latter approaches are considered particularly attractive. Since, however, the hand-coding of robust antecedent filtering strategies such as syntactic disjoint reference and agreement in person, number, and gender constitutes a once-for-all effort, the question arises whether at all they should be derived automatically. In this paper, it is investigated what might be gained by combining the best of two worlds: designing the universally valid antecedent filtering strategies manually, in a once-for-all fashion, and deriving the (potentially genre-specific) antecedent selection strategies automatically by applying machine-learning techniques. An anaphor resolution system ROSANA-ML, which follows this paradigm, is designed and implemented. Through a series of formal evaluations, it is shown that, while exhibiting additional advantages, ROSANAML reaches a performance level that compares with the performance of its manually designed ancestor ROSANA.