Informatik
Refine
Year of publication
Document Type
- Preprint (747)
- Article (400)
- Working Paper (119)
- Doctoral Thesis (92)
- Diploma Thesis (46)
- Conference Proceeding (41)
- Book (37)
- Bachelor Thesis (35)
- diplomthesis (29)
- Report (25)
- Part of a Book (13)
- Contribution to a Periodical (10)
- Master's Thesis (6)
- Habilitation (1)
- Lecture (1)
- Review (1)
Has Fulltext
- yes (1603)
Is part of the Bibliography
- no (1603)
Keywords
Institute
- Informatik (1603)
- Frankfurt Institute for Advanced Studies (FIAS) (1001)
- Physik (982)
- Mathematik (55)
- Präsidium (41)
- Medizin (25)
- Biowissenschaften (21)
- Exzellenzcluster Makromolekulare Komplexe (8)
- Psychologie (8)
- Deutsches Institut für Internationale Pädagogische Forschung (DIPF) (5)
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.