Kaiserslautern - Fachbereich Informatik
Refine
Year of publication
Document Type
- Report (139) (remove)
Has Fulltext
- yes (139)
Keywords
- Dienstgüte (3)
- Formalisierung (3)
- AG-RESY (1)
- AKLEON (1)
- Ad-hoc-Netz (1)
- Compiler (1)
- Coq (1)
- Extraction (1)
- Formal Semantics (1)
- Fräsen (1)
- Funknetz (1)
- Hals-Nasen-Ohren-Chirurgie (1)
- Hals-Nasen-Ohren-Heilkunde (1)
- Hub-and-Spoke-System (1)
- Hörgerät (1)
- Implantation (1)
- Isabelle/HOL (1)
- Kommunikationsprotokoll (1)
- Komplexitätsklasse NP (1)
- META-AKAD (1)
- Mapping (1)
- Mastoid (1)
- Mastoidektomie (1)
- Model Checking (1)
- NP-hard (1)
- OCL 2.0 (1)
- Ohrenchirurgie (1)
- Peer-to-Peer-Netz (1)
- Profiles (1)
- RONAF (1)
- Regelung (1)
- Reservierungsprotokoll (1)
- Roboter (1)
- Routing (1)
- SDL (1)
- SDL-2000 (1)
- Schädelchirurgie (1)
- Spezifikation (1)
- Sprachprofile (1)
- System Abstractions (1)
- Translation Validation (1)
- UML 2 (1)
- UML Profile (1)
- aliasing (1)
- bedingte Aktionen (1)
- compiler (1)
- domains (1)
- encapsulation (1)
- guarded actions (1)
- hub location (1)
- mastoid (1)
- mastoidectomy (1)
- object-orientation (1)
- otorhinolaryngological surgery (1)
- ownership (1)
- synchrone Sprachen (1)
- synchronous languages (1)
- theorem prover (1)
- translation validation (1)
- types (1)
Faculty / Organisational entity
Wireless LANs operating within unlicensed frequency bands require random access schemes such as CSMA/ CA, so that wireless networks from different administrative domains (for example wireless community networks) may co-exist without central coordination, even when they happen to operate on the same radio channel. Yet, it is evident that this Jack of coordination leads to an inevitable loss in efficiency due to contention on the MAC layer. The interesting question is, which efficiency may be gained by adding coordination to existing, unrelated wireless networks, for example by self-organization. In this paper, we present a methodology based on a mathematical programming formulation to determine the
parameters (assignment of stations to access points, signal strengths and channel assignment of both access points and stations) for a scenario of co-existing CSMA/ CA-based wireless networks, such that the contention between these networks is minimized. We demonstrate how it is possible to solve this discrete, non-linear optimization problem exactly for small
problems. For larger scenarios, we present a genetic algorithm specifically tuned for finding near-optimal solutions, and compare its results to theoretical lower bounds. Overall, we provide a benchmark on the minimum contention problem for coordination mechanisms in CSMA/CA-based wireless networks.
On the Complexity of the Uncapacitated Single Allocation p-Hub Median Problem with Equal Weights
(2007)
The Super-Peer Selection Problem is an optimization problem in network topology construction. It may be cast as a special case of a Hub Location Problem, more exactly an Uncapacitated Single Allocation p-Hub Median Problem with equal weights. We show that this problem is still NP-hard by reduction from Max Clique.
W-Lisp Sprachbeschreibung
(1993)
W-Lisp [Wippennann 91] ist eine Sprache, die im Bereich der Implementierung höherer
Programmiersprachen verwendet wird. Ihre Anwendung ist nicht auf diesen Bereich beschränkt. Gute Lesbarkeit der W-Lisp-Notation wird durch zahlreiche Anleihen aus dem Bereich der bekannten imperativen Sprachen erzielt. W-Lisp-Programme können im Rahmen eines Common Lisp-Systems ausgeführt werden. In der WLisp Notation können alle Lisp-Funktionen (inkl. MCS) verwendet werden, so daß die Mächtigkeit von Common-Lisp [Steele 90] in dieser Hinsicht auch in W-Lisp verfügbar ist.
Neuronale Netze sind ein derzeit (wieder) aktuelles Thema. Trotz der oft eher schlagwortartigen
Verwendung dieses Begriffs beinhaltet er eine Vielfalt von Ideen, unterschiedlichste methodische
Ansätze und konkrete Anwendungsmöglichkeiten. Die grundlegenden Vorstellungen sind dabei nicht neu, sondern haben eine mitunter recht lange Tradition in angrenzenden Disziplinen wie Biologie, Kybernetik , Mathematik und Physik . Vielversprechende Forschungsergebnisse der letzten Zeit haben dieses Thema wieder in den Mittelpunkt des Interesses gerückt und eine Vielzahl neuer Querbezüge zur Informatik und Neurobiologie sowie zu anderen, auf den ersten Blick weit entfernten Gebieten offenbart. Gegenstand des Forschungsgebiets Neuronale Netze ist dabei die Untersuchung und Konstruktion informationsverarbeitender Systeme, die sich aus vielen mitunter nur sehr primitiven, uniformen Einheiten zusammensetzen und deren wesentliches Verarbeitungsprinzip die Kommunikation zwischen diesen Einheiten ist, d.h. die Übertragung von Nachrichten oder Signalen. Ein weiteres
Charakteristikum dieser Systeme ist die hochgradig parallele Verarbeitung von Information innerhalb
des Systems. Neben der Modellierung kognitiver Prozesse und dem Interesse, wie das menschliche Gehirn komplexe kognitive Leistungen vollbringt, ist über das rein wissenschaftliche Interesse hinaus in zunehmendem Maße auch der konkrete Einsatz neuronaler Netze in verschiedenen technischen Anwendungsgebieten zu sehen. Der vorliegende Report beinhaltet die schriftlichen Ausarbeitungen der Teilnehmerinnen des Seminars Theorie und Praxis neuronaler Netze , das von der Arbeitsgruppe Richter im Sommersemester 1993 an der Universität Kaiserslautern veranstaltet wurde. Besonderer Wert wurde darauf gelegt, nicht nur die theoretischen Grundlagen neuronaler Netze zu behandeln, sondern auch deren Einsatz in der Praxis zu diskutieren. Die Themenauswahl spiegelt einen Teil des weiten Spektrums der Arbeiten auf diesem Gebiet wider. Ein Anspruch auf Vollständigkeit kann daher nicht erhoben werden. Insbesondere sei darauf verwiesen, daß für eine intensive, vertiefende Beschäftigung mit einem Thema auf die jeweiligen Originalarbeiten zurückgegriffen werden sollte. Ohne die Mitarbeit der Teilnehmerinnen und Teilnehmer des Seminars wäre dieser Report nicht möglich gewesen. Wir bedanken uns daher bei Frank Hauptmann, Peter Conrad, Christoph Keller, Martin Buch, Philip Ziegler, Frank Leidermann, Martin Kronenburg, Michael Dieterich, Ulrike Becker, Christoph Krome, Susanne Meyfarth , Markus Schmitz, Kenan Çarki, Oliver Schweikart, Michael Schick und Ralf Comes.
This report presents a generalization of tensor-product B-spline surfaces. The new scheme permits knots whose endpoints lie in the interior of the domain rectangle of a surface. This allows local refinement of the knot structure for approximation purposes as well as modeling surfaces with local tangent or curvature discontinuities. The surfaces are represented in terms of B-spline basis functions, ensuring affine invariance, local control, the convex hull property, and evaluation by de Boor's algorithm. A dimension formula for a class of generalized tensor-product spline spaces is developed.
In this article we present a method to generate random objects from a large variety of combinatorial classes according to a given distribution. Given a description of the combinatorial class and a set of sample data our method will provide an algorithm that generates objects of size n in worst-case runtime O(n^2) (O(n log(n)) can be achieved at the cost of a higher average-case runtime), with the generated objects following a distribution that closely matches the distribution of the sample data.
Ein maßgeschneidertes Kommunikationssystem für eine mobile Applikation mit Dienstgüteanforderungen
(2004)
In diesem Beitrag wird die Maßschneiderung eines Ad-Hoc-Kommunikationssystems zur Fernsteuerung eines Luftschiffs über WLAN vorgestellt. Dabei steht die Dienstunterstützung bei der Übertragung mehrerer Datenströme im Vordergrund. Es werden verschiedene Dienstgütemechanismen erklärt und deren Entwicklung und Integration in ein Kommunikationsprotokoll mit Hilfe eines komponentenbasierten Ansatzes genauer erläutert.
We present a methodology to augment system safety step-by-step and illustrate the approach by the definition of reusable solutions for the detection of fail-silent nodes - a watchdog and a heartbeat. These solutions can be added to real-time system designs, to protect against certain types of system failures. We use SDL as a system design language for the development of distributed systems, including real-time systems.
Interactive graphics has been limited to simple direct illumination that commonly results in an artificial appearance. A more realistic appearance by simulating global illumination effects has been too costly to compute at interactive rates. In this paper we describe a new Monte Carlo-based global illumination algorithm. It achieves performance of up to 10 frames per second while arbitrary changes to the scene may be applied interactively. The performance is obtained through the effective use of a fast, distributed ray-tracing engine as well as a new interleaved sampling technique for parallel Monte Carlo simulation. A new filtering step in combination with correlated sampling avoids the disturbing noise artifacts common to Monte Carlo methods.
Die Sichten von Projektmitgliedern auf Prozesse von Software-Entwicklungen sollen in der Prozeßmodellierungssprache MVP-L formuliert und anschließend in ein Umfassendes Prozeßmodell integriert werden. Dabei ist die Identifikation ähnlicher Informationen in verschiedenen Sichten von Bedeutung. In dieser Arbeit berichten
wir über die Adaption und Synthese verschiedener Ansätze zum Thema Ähnlichkeit aus unterschiedlichen Domänen (Schema-Integration beim Datenbank-Entwurf, Analoges und Fallbasiertes Schließen, Wiederverwendung und System-Spezifikation). Das Ergebnis, die Ähnlichkeitsfunktion vsim, wird anhand eines Referenzbeispiels illustriert. Dabei gehen wir insbesondere auf die Eigenschaft der Funktion vsim ein und berichten über Erfahrungen im Umgang mit dieser Funktion zur Berechnung der Ähnlichkeit zwischen Prozeßmodellen.
There is a well known relationship between alternating automata on finite words and symbolically represented nondeterministic automata on finite words. This relationship is of practical relevance because it allows to combine the advantages of alternating and symbolically represented nondeterministic automata on finite words. However, for infinite words the situation is unclear. Therefore, this work investigates the relationship between alternating omega-automata and symbolically represented nondeterministic omega-automata. Thereby, we identify classes of alternating omega-automata that are as expressive as safety, liveness and deterministic prefix automata, respectively. Moreover, some very simple symbolic nondeterminisation procedures are developed for the classes corresponding to safety and liveness properties.
Estelle is an internationally standardized formal description technique (FDT) designed for the specification of distributed systems, in particular communication protocols. An Estelle specification describes a system of communicating components (module instances). The specified system is closed in a topological sense, i.e. it has no ability to interact with some environment. Because of this restriction, open systems can only be specified together with and incorporated with an environment. To overcome this restriction, we introduce a compatible extension of Estelle, called "Open Estelle". It allows the specification of (topologically) open systems, i.e. systems that have the ability to communicate with any environment through a well-defined external interface. We define aformal syntax and a formal semantics for Open Estelle, both based on and extending the syntax and semantics of Estelle. The extension is compatible syntactically and semantically, i.e. Estelle is a subset of Open Estelle. In particular, the formal semantics of Open Estelle reduces to the Estelle semantics in the special case of a closed system. Furthermore, we present a tool for the textual integration of open systems into environments specified in Open Estelle, and a compiler for the automatic generation of implementations directly from Open Estelle specifications.
Formale Beschreibungstechniken (FDTs) erlauben durch ihre formale Syntax und Semantik eine präzise Systembeschreibung und sind Grundlage für die formale Verifikation. Bei der Implementierung von Systemen wird jedoch nach wie vor von Hand implementiert, selbst wenn ausgereifte Werkzeuge zur automatischen Generierung von Kode direkt aus der formalen Spezifikation existieren. Die Ursache dafür liegt in dem Ruf dieser Werkzeuge, Kode mit extrem geringer Leistungsfähigkeit zu erzeugen. Es gibt jedoch kaum quantitative Leistungsvergleiche zwischen manuell und automatisch generierten Implementierungen, die dieses Vorurteil stützen oder widerlegen könnten. In diesem Beitrag wird ein solcher Leistungsvergleich anhand des Hochleistungsprotokolls XTP und der FDT Estelle vorgestellt. Er liefert eine Bestandsaufnahme des momentanen Entwicklungsstandes bei der automatischen Generierung von Kode aus Estelle-Spezifikationen im direkten Vergleich zu gut optimierten Handimplementierungen. Es zeigt sich, daß in dem betrachteten Fall eines komplexen Protokolls die Handimplementierung zwar merklich leistungsstärker ist. Dieser Leistungsvorteil wird jedoch durch einen sehr hohen Implementierungsaufwand sowie die Schwierigkeit, die Korrektheit bzgl. der Spezifikation sicherzustellen, erkauft. Im einzelnen Anwendungsfall kann es daher trotz der Leistungseinbußen durchaus vorteilhaft sein, automatisch Kode zu erzeugen, zumal in der Bestandsaufnahme festgestellt wurde, daß automatisch generierte Implementierungen z.T. besser abschneiden als erwartet. Zudem besteht - anders als bei der bereits umfassend optimierten Handimplementierung - noch ein erhebliches ungenutztes Potential zur Leistungsverbesserung der automatisch generierten Implementierung.
Ownership Domains generalize ownership types. They support programming patterns like iterators that are not possible with ordinary ownership types. However, they are still too restrictive for cases in which an object X wants to access the public domains of an arbitrary number of other objects, which often happens in observer scenarios. To overcome this restriction, we developed so-called loose domains which abstract over several precise domains. That is, similar to the relation between supertypes and subtypes we have a relation between loose and precise domains. In addition, we simplified ownership domains by reducing the number of domains per object to two and hard-wiring the access permissions between domains. We formalized the resulting type system for an OO core language and proved type soundness and a fundamental accessibility property.
In den Modellierungssystemen des CAD/CAM werden oft unterschiedliche Methoden zur mathematischen Beschreibung von Freiformkurven und -flächen eingesetzt. Als Basisfunktionen können sowohl Monome, Bernstein-Polynome, B-Spline-Basisfunktionen als auch nicht lineare Funktionen auftreten. In den einzelnen CAD-Systemen kann der maximal zulässige Grad dieser Basisfunktionen variieren. Müssen nun Daten zwischen verschiedenen CAD-Systemen ausgetauscht werden, so muß u. U. eine Basistransformation
und/oder eine Gradanpassung durchgeführt werden. Diese Transformationen sind i.a. nicht exakt möglich. Hier sind geeignete, möglichst optimale Approximationen nötig. Bisher wurden verschiedene Verfahren entwickelt. Das älteste geht zurück auf Forrest [Forr72]. Farin [FAR90] invertiert den Prozeß der Graderhöhung. Watkins und Worsey [Wat88] sowie Lachance [Lach88] reduzieren den Polynomgrad in der Tschebyscheff-Basis. Hoschek et al. [Hos89] sowie Plass und Stone [Plas83] approximieren die Kurve bzw. Fläche punktweise. Dadurch lassen sich alle Kurven- und Flächenrepräsentationen durch eine Bézier-Darstellung approximieren. Ein Approximationsfehler kann jedoch auch nur punktweise garantiert werden. Durch einen anschließenden Parameteriterationsprozeß läßt sich eine weitere Approximationsverbesserung erzielen. Eine solche Parameterkorrektur ist jedoch nur dann sinnvoll, wenn die Parametrisierung der Approximationskurve bzw. -fläche frei gewählt werden kann. In Fällen, in denen die Funktionswerte dei; zu approximierenden Flächen bzgl. ihrer Parameterwerte mit anderen Flächen korrespondieren, darf keine Parameteränderung durchgeführt werden, wie z.B. bei der Approximation sogenannter Eigenschaftsflächen, die eine bestimmte Eigenschaft einer anderen Fläche, wie etwa die Gausskrümmung oder die Normalenrichtung darstellen. In dieser Arbeit wird ein Verfahren zur optimalen Gradreduktion von Bézierkurven und -flächen vorgestellt. Damit eine \(C^0\)-stetige Approximation innerhalb einer vom Benutzer vorgegebenen Fehlertoleranz durchgeführt werden kann, muß die Approximation mindestens eine Berührordnung ersten Grades mit der Originalkurve bzw. -fläche aufweisen. Mit Hilfe arithmetischer Operationen auf Bézierdarstellungen [Faro88], [Schr92] werden lineare Gleichungssysteme für eine optimale Belegung der freien Parameter aufgestellt, sowie eine Fehlerkurve bzw. -fläche in Bézierform berechnet, um die Einhaltung einer Fehlertoleranz zu gewährleisten.
In der CAGD Literatur werden häufig Ableitungen und Graderhöhungen von Bezierkurven und -flächen wiederum in Bezierform angegeben [1][2][3][6]. Meistens werden diese Darstellungen nur für theoretische Betrachtungen verwendet, z.B. geometrischer Deutung von Stetigkeiten zwischen angrenzenden Flächenstücken. Für praktische Anwendungen reicht die Menge der Operationen jedoch nicht aus. Farouki und Rajan [4] zeigten, daß die Resultate arithmetischer Operationen, wie Addition und Multiplikation auf Bezierkurven auch als Bezierkurven darstellbar sind. Hier werden wir die Operationen auf polynomiale und rationale Tensorprodukt Bezierflächen und Flächen über Dreiecken ausdehnen. Eine Erweiterung auf rationale Flächen ermöglicht insbesondere die Ausführung einer Division, wie sie für viele Anwendungen benötigt wird. Das Rechnen mit Flächen hat im Gegensatz zu punktweisen Auswertungen den Vorteil gleichzeitig mit Hilfe von notwendigen Bedingungen an das entstandene Beziernetz sichere Ergebnisabschätungen angeben zu können. Diese lassen sich für adaptive Verfahren nutzen und sind insbesondere dort wichtig, wo es auf exakte Aussagen über das Verhalten von Flächen ankommt, wie z.B. bei der Qualitätsanalyse von Freiformflächen [5]. Mit Hilfe der hier vorgestellten Operationen läßt sich u.a. an Vorzeichenwechseln erkennen, ob eine zu untersuchende Bezierfläche konvex ist oder nicht (siehe Kapitel 4). Außerdem können Fehler, die bei punktweisen Auswertungen auf Gittern mit großer Maschenweite entstehen, vermieden werden. Nachdem in Kapitel 2 die zum Verständnis nötigen Definitionen und Schreibweisen erläutert wurden, werden in Kapitel 3 die grundlegenden Operationen für eine Arithmetik
auf Bezierflächen beschrieben. Dabei werden Formeln angegeben, die die Bezierpunkte und Gewichte der Ergebnisfläche aus denen der Operandenflächen bestimmen. Durch Aneinanderreihung und Verkettung einzelner Operationen lassen sich dann komplexe Berechnungen mit der gesamten Fläche ausführen. Zum Schluß werden in Kapitel 4 einige Beispiele aus dem Bereich der Qualitätsanalyse von Freiformflächen angegeben.
This paper describes some new algorithms for the accurate calculation of surface properties. In the first part an arithmetic on Bézier surfaces is introduced. Formulas are given, which determine the Bézier points and weights of the resulting surface from the points and weights of the operand surfaces. An application of the arithmetic operations to the surface interrogation methods are described in the second part. It turns out, that the quality analysis can be reduced to a few numerical stable operations. Finally the advantages and disadvantages of this method are discussed.
Partitioned chain grammars
(1979)
This paper introduces a new class of grammars, the partitioned chain grammars, for which efficient parsers can be automatically generated. Besides being efficiently parsable these grammars possess a number of other properties, which make them very attractive for the use in parser-generators. They for instance form a large grammarclass and describe all deterministic context-free languages. Main advantage of the partitioned chain grammars however is, that given a language it is usually easier to describe it by a partitioned chain grammar than to construct a grammar of some other type commonly used in parser-generators for it.
On Abstract Shapes of RNA
(2008)
As any RNA sequence can be folded in many different ways, there are lots of different possible secondary structures for a given sequence. Most computational prediction methods based on free energy minimization compute a number of suboptimal foldings and we have to identify the native structures among all these possible secondary structures. For this reason, much effort has been made to develop approaches for identifying good predictions of RNA secondary structure. Using the abstract shapes approach as introduced by Giegerich et al., each class of similar secondary structures is represented by one shape and the native structures can be found among the top shape representatives. In this article, we derive some interesting results answering enumeration problems for abstract shapes and secondary structures of RNA. We start by computing symptotical representations for the number of shape representations of length n. Our main goal is to find out how much the search space can be reduced by using the concept of abstract shapes. To reach this goal, we analyze the number of secondary structures and shapes compatible with an RNA sequence of length n under the assumption that base pairing is allowed between arbitrary pairs of bases analytically and compare their exponential growths. Additionally, we analyze the number of secondary structures compatible with an RNA sequence of length n under the assumptions that base pairing is allowed only between certain pairs of bases and that the structures meet some appropriate conditions. The exponential growth factors of the resulting asymptotics are compared to the corresponding experimentally obtained value as given by Giegerich et al.
This article focuses on the analytical analysis of the free energy in a realistic model for RNA secondary structures. In fact, the free energy in a stochastic model derived from a database of small and large subunit ribosomal RNA (SSU and LSU rRNA) data is studied. A common thermody-namic model for computing the free energy of a given RNA secondary structure, as well as stochastic context-free grammars and generating functions are used to derive the desired results. These results include asymptotics for the expected free energy and for the corresponding variance of a random RNA secondary structure. The quality of our model is judged by comparing the derived results to the used database of SSU and LSU rRNA data. At the end of this article, it is discussed how our results could be used to help on identifying good predictions of RNA secondary structure.
Software-Projekte bestehen aus einer Vielzahl von Teilaufgaben, die durch komplexe Wechselbeziehungen miteinander verknüpft sind. Systematische Unterstützung bei der Durchführung von Software-Projekten erfordert deshalb nicht nur die isolierte Unterstützung einzelner Teilaufgaben, sondern insbesondere der Wechselbeziehungen. Außerdem müssen Aktivitäten des Messens und Bewertens durchgeführt werden, um quantitative Aussagen über Produkte und Prozesse ableiten zu können. Ziel des MVP-Projekts (Multi-View Process modeling) ist es, derartige integrierte Unterstützung auf der Basis meßbarer Projektpläne zur Verfügung zu stellen. Projektpläne setzen sich dabei unter anderem aus Prozeß-, Produkt-, Ressourcen- und Qualitätsmodellen zusammen. Meßansätze werden nicht nur zur systematischen Unterstützung von Projekten, sondern auch zur Verbesserung existierender Prozeß-, Produkt-, Ressource- und Qualitätsmodelle aufgrund 'gemessener' Erfahrungswerte verwendet. Die Benutzer des MVP-Entwicklungssystems (MVP-S) werden durch ihre Rollen im Rahmen eines Projekts charakterisiert werden können. Es wird beschrieben, wie Rollen das MVP-System nutzen können. Dies geschieht entweder durch direkte Repräsentation ihrer Aufgaben als Prozesse oder indem die im Projektplan repräsentierte Information ausgewertet und präsentiert wird; entsprechend bezeichnen wir eine Rolle als "zustandsverändernd" oder als "zustandserfragend". Um diese Rollen zu unterstützen, existieren unterschiedliche Möglichkeiten abhängig vom Grad der Automatisierung. Es werden beispielhaft drei Stufen aufgezeigt. Anschließend wird die Realisierung einer prototypischen, qualitätsorientierten, prozeßsensitiven Software-Entwicklungsumgebung diskutiert. Zum Abschluß wird auf gegenwärtige und zukünftige Forschungsfragen im Rahmen des MVP-Projekts eingegangen.
The intuitionistic calculus mj for sequents, in which no other logical symbols than those for implication and universal quantification occur, is introduced and analysed. It allows a simple backward application, called mj-reduction here, for searching for derivation trees. Terms needed in mj-reduction can be found with the unification algorithm. mj-Reduction with unification can be seen as a natural extension of SLD-resolution. mj-Derivability of the sequents considered here coincides with derivability in Johansson's minimal intuitionistic calculus LHM in [6]. Intuitionistic derivability of formulae with negation and classical derivability of formulae with all usual logical symbols can be expressed with mj-derivability and hence be verified by mj-reduction. mj-Derivations can be easily translated into LJ-derivations without
"Schnitt", or into NJ-derivations in a slightly sharpened form of Prawitz' normal form. In the first three sections, the systematic use of mj-reduction for proving in predicate logic is emphasized. Although the fourth section, the last and largest, is exclusively devoted to the mathematical analysis of the calculus mj, the first three sections may be of interest to a wider readership, including readers looking for applications of symbolic logic. Unfortunately, the mathematical analysis of the calculus mj, as the study of Gentzen's calculi, demands a large amount of technical work that obscures the natural unfolding of the argumentation. To alleviate this, definitions and theorems are completely embedded in the text to provide a fluent and balanced mathematical discourse: new concepts are indicated with bold-face, proofs of assertions are outlined, or omitted when it is assumed that the reader can provide them.
Skelettbasierte implizite Flächen haben aufgrund ihrer Fähigkeit, durch automatisches Verschmelzen aus wenigen, einfachen Primitiven komplexe Strukturen zu formen, für Modellierung, Visualisierung und Animation zunehmend an Bedeutung gewonnen. Eine wesentliche Schwierigkeit beim Einsatz impliziter Flächen ist nach wie vor eine effiziente Visualisierung der resultierenden Objekte. In der vorliegenden
Arbeit werden die grundlegenden Ideen einer Methode zur partikelgestützten Triangulierung skelettbasierter impliziter Flächen beschrieben, die die Vorteile einer partikelgestützten Abtastung
impliziter Flächen mit der polygonalen Darstellung durch Dreiecke kombiniert. Der Algorithmus ist in der Lage, effizient auf dynamische Veränderungen der Gestalt sowie das Auseinanderreißen nicht allzu
komplexer implizit gegebener Objekte zu reagieren. Zusätzlich besteht die Möglichkeit, die Triangulierung krümmungsadaptiv zu gestalten, um bei gleichbleibender Darstellungsqualität eine Reduktion der Dreiecksanzahl zu erreichen.
A natural extension of SLD-resolution is introduced as a goal directed proof procedure
for the full first order implicational fragment of intuitionistic logic. Its intuitionistic semantic fits a procedural interpretation of logic programming. By allowing arbitrary nested implications it can be used for implementing modularity in logic programs. With adequate negation axioms it gives an alternative to negation as failure and leads to a proof procedure for full first order predicate logic.
The use of non-volatile semiconductor memory within an extended storage hierarchy promises significant performance improvements for transaction processing. Although page-addressable semiconductor memories like extended memory, solid-state disks and disk caches are commercially available since several years, no detailed investigation of their use for transaction processing has been performed so far. We present a comprehensive simulation study that compares the performance of these storage types and of different usage forms. The following usage forms are considered: allocation of entire log and database files in non-volatile semiconductor memory, using a so-called write buffer to perform disk writes asynchronously, and caching of database pages at intermediate storage levels (in addition to main memory caching). Our simulations are conducted with both synthetically generated workloads and traces from real-life database applications. In particular, simulation results will be presented for the debit-credit workload frequently used in transaction processing benchmarks. As expected, the greatest performance improvements (but at the highest cost) can be achieved by storing log and database files completely in non-volatile semiconductor memory. For update-intensive
workloads, a limited amount of non-volatile memory used as a write buffer also proved to be very effective. To reduce the number of disk reads; caching of database pages in addition to main memory is best supported by an extended memory buffer. In this respect, disk caches are found to be less effective as they are designed for one-level caching. Different storage costs suggest that it may be cost-effective to use two or even three of the intermediate storage types together. The performance improvements obtainable by the use of non-volatile semiconductor memory is also found to reduce the need for sophisticated DBMS buffer management in order to achieve high transaction processing performance.
The rapid development of any field of knowledge brings with it unavoidable fragmentation and proliferation of new disciplines. The development of computer science is no exception. Software engineering (SE) and human-computer interaction (HCI) are both relatively new disciplines of computer science. Furthermore, as both names suggest, they each have strong connections with other subjects. SE is concerned with methods and tools for general software development based on engineering principles. This discipline has its roots not only in computer science but also in a number of traditional engineering disciplines. HCI is concerned with methods and tools for the development of human-computer interfaces, assessing the usability of computer systems and with broader issues about how people interact with computers. It is based on theories about how humans process information and interact with computers, other objects and other people in the organizational and social contexts in
which computers are used. HCI draws on knowledge and skills from psychology, anthropology and sociology in addition to computer science. Both disciplines need ways of measuring how well their products and development processes fulfil their intended requirements. Traditionally SE has been concerned with 'how software is constructed' and HCI with 'how people use software'. Given the
different histories of the disciplines and their different objectives, it is not surprising that they take different approaches to measurement. Thus, each has its own distinct 'measurement culture.' In this paper we analyse the differences and the commonalties of the two cultures by examining the measurement approaches used by each. We then argue the need for a common measurement taxonomy and framework, which is derived from our analyses of the two disciplines. Next we demonstrate the usefulness of the taxonomy and framework via specific example studies drawn from our own work and that of others and show that, in fact, the two disciplines have many important similarities as well as differences and that there is some evidence to suggest that they are growing closer. Finally, we discuss the role of the taxonomy as a framework to support: reuse, planning future studies, guiding practice and facilitating communication between the two disciplines.
Optimization of Projection Methods for Solving ill-posed Problems. In this paper we propose a modification of the projection scheme for solving ill-posed problems. We show that this modification allows to obtain the best possible order of accuracy of Tikhonov Regularization using an amount of information which is far less than for the standard projection technique.
In this paper we show how Metropolis Light Transport can be extended both in the underlying theoretical framework and the algorithmic implementation to incorporate volumetric scattering.
We present a generalization of the path integral formulation thathandles anisotropic scattering in non-homogeneous media. Based on this framework we introduce a new mutation strategy that is
specifically designed for participating media. It exploits the locality of light propagation by perturbing certain interaction points within the medium. To efficiently sample inhomogeneous media a new ray marching method has been developed that avoids aliasing artefacts and is significantly faster than stratified sampling. The resulting global illumination algorithm provides a physically correct simulation of light transport in the presence of participating media that includes effects such as volume caustics and multiple volume scattering. It is not restricted to certain classes of geometry and scattering models and has minimal memory requirements. Furthermore, it is unbiased and robust, in the sense that it produces satisfactory results for a wide range of input scenes and lighting situations within acceptable time bounds. In particular, we found that it is weil suited for complex scenes with many light sources.
One of the fundamental problems in computational structural biology is the prediction of RNA secondary structures from a single sequence. To solve this problem, mainly two different approaches have been used over the past decades: the free energy minimization (MFE) approach which is still considered the most popular and successful method and the competing stochastic context-free grammar (SCFG) approach. While the accuracy of the MFE based algorithms is limited by the quality of underlying thermodynamic models, the SCFG method abstracts from free energies and instead tries to learn about the structural behavior of the molecules by training the grammars on known real RNA structures, making it highly dependent on the availability of a rich high quality training set. However, due to the respective problems associated with both methods, new statistics based approaches towards RNA structure prediction have become increasingly appreciated. For instance, over the last years, several statistical sampling methods and clustering techniques have been invented that are based on the computation of partition functions (PFs) and base pair probabilities according to thermodynamic models. A corresponding SCFG based statistical sampling algorithm for RNA secondary structures has been studied just recently. Notably, this probabilistic method is capable of producing accurate (prediction) results, where its worst-case time and space requirements are equal to those of common RNA folding algorithms for single sequences.
The aim of this work is to present a comprehensive study on how enriching the underlying SCFG by additional information on the lengths of generated substructures (i.e. by incorporating length-dependencies into the SCFG based sampling algorithm, which is actually possible without significant losses in performance) affects the reliability of the induced RNA model and the accuracy of sampled secondary structures. As we will see, significant differences with respect to the overall quality of generated sample sets and the resulting predictive accuracy are typically implied. In principle, when considering the more specialized length-dependent SCFG model as basis for statistical sampling, a higher accuracy of predicted foldings can be reached at the price of a lower diversity of generated candidate structures (compared to the more general traditional SCFG variant or sampling based on PFs that rely on free energies).
For most applications the used transport service providers are predetermined during the development of the application. This makes it difficult to consider the application communication requirements and to exploit specific features of the network technology. Specialized protocols that are more efficient and offer a qualitative improved service are typically not supported by most applications because they are not commonly available. In this paper we propose a concept for the realization of protocol independent transport services. Only a transport service is predetermined during the development of the application and an appropriate transport service provider is dynamically selected at run time. This enables to exploit specialized protocols if possible, but standard protocols could still be used if necessary. The main focus of this paper is how a transport service could provide a new transport service provider transparently to existing applications. A prototype is presented that maps TCP/IP based applications to an ATM specific transport service provider which offers a reliable and unreliable transport service like TCP/IP.
The Analytic Blossom
(2001)
Blossoming is a powerful tool for studying and computing with Bézier and B-spline curves and surfaces - that is, for the investigation and analysis of polynomials and piecewise polynomials in geometric modeling. In this paper, we define a notion of the blossom for Poisson curves. Poisson curves are to analytic functions what Bézier curves are to polynomials - a representation adapted to geometric design. As in the polynomial setting, the blossom provides a simple, powerful, elegant and computationally meaningful way to analyze Poisson curves. Here, we
define the analytic blossom and interpret all the known algorithms for Poisson curves - subdivision, trimming, evaluation of the function and its derivatives, and conversion between the Taylor and the Poisson basis - in terms of this analytic blossom.
This document introduces the extension of Katja to support position structures and explains the subtleties of their application as well as the design decisions made and problems solved with respect to their implementation. The Katja system was first introduced by Jan Schäfer in the context of his project work and is based on the MAX system developed by Arnd Poetzsch-Heffter.
Katja is a tool generating order-sorted recursive data types as well as position types for Java, from specifications using an enhanced ML like notation. Katja’s main features are its conciseness of specifications, the rich interface provided by the generated code and the Java atypical immutability of types. After several stages of extending and maintaining the Katja project, it became apparent many changes had to be done. The original design of Katja wasn’t prepared for the introduction of several backends, the introduction of position sorts and constant feature enhancements and bug fixes. By supplying this report Katja reaches release status for the first time.
Mobile Agenten im Internet
(2001)
Mobile Agenten haben sich in den letzten Jahren zunehmend in der Architektur und Programmierung verteilter Systeme bewährt. Es sind Programme, die einen Internen Zustand mit sich führen, während sie verschiedene, möglicherweise auf unterschiedlichen Plattformen basierende, Systeme besuchen. Auf dem jeweiligen System nehmen sie Dienste in Anspruch, indem sie entweder lokale Bibliotheken ansprechen, oder auf durch das System bereitgestellte Dienste zugreifen. Dabei müssen mobile Agenten sowohl alle vom Programm benötigten Daten, wie auch den gesamten Code mit sich führen. Zwar sind die Daten ein wichtiger (wenn nicht sogar der entscheidende) Teil eines Agenten, trotzdem wird in der Regel nicht als wertvoller, eigenständiger Part angesehen. Dies ist jedoch nicht immer ratsam, könnten doch Agenten am aktuellen Aufenthaltsort einen „Container" zurückzulassen um ihm anderen Agenten zur Verfügung zu stellen (natürlich erst nach erfolgter Zugriffskontrolle), bzw. die Daten erst dann auf ein Migrationsziel übertragen, wenn sich durch lokale Aufrufe des Systems herausgestellt hat, dass sie dort benötigt werden. Diese Arbeit ist zweigeteilt, insofern, als dass sie sich mit den zwei verschiedenen „Ebenen" der mobilen Agenten beschäftigt. Im ersten Teil werden die für die Migration und Nutzung der Resourcen notwendigen Aspekte besprochen. Dabei wird der Schwerpunkt auf die notwendige Unterstützung durch die Umgebung gelegt, wobei nicht eine neue integrierte Umgebung entworfen, sondern vielmehr die notwendigen Blöcke aufgezeigt werden sollen. Diese können dann als Teil eines Environments oder aber als eigentständige Komponente bereitsgestellt werden. Der zweite Teil beschäftigt sich mit den durch die Interaktion verschiedener Agenten entstehenden Probleme. Stichworte hierbei sind die Kostenkontrolle (wer bezahlt auf welche Art für in Anspruch genommene Dienste), Workflow Unterstützung, sowie Sicherheit in einem offenen, verteilten System, in dem es keine zentrale Überprüfung von Rechten und Identitäten geben kann. Abgeschlossen wird diese Ausarbeitung mit einer Bewertung der auf den beiden Ebenen gefundenen Problemen und Eigenheiten, wobei dann die Frage aufgeworfen wird, ob Agenten in der heutigen Form überhaupt sinnvoll sind.
Web-based authentication is a popular mechanism implemented by Wireless Internet Service Providers (WISPs) because it allows a simple registration and authentication of customers, while avoiding the high resource requirements of the new IEEE 802.11i security standard and the backward compatibility issues of legacy devices. In this work we demonstrate two different and novel attacks against web-based authentication. One attack exploits operational anomalies of low- and middle-priced devices in order to hijack wireless clients, while the other exploits an already known vulnerability within wired-networks, which in dynamic wireless environments turns out to be even harder to detect and protect against.
In dieser Arbeit beschreiben wir einen Ansatz zur automatischen Synthese zustandsendlicher, reaktiver Systeme, ausgehend von einer rein deklarativen, logischen Spezifikation. Dazu verwenden wir temporal stratifizierte Programme,
das sind spezielle Logik-Programme auf der Grundlage einer linearen, temporalen Aussagenlogik. Die Umgebung eines zu implementierenden Steuerungsprogrammes wird hier durch eine Menge von PROLOG-ähnlichen Programmklauseln beschrieben; zusätzlich wird eine Sicherheitsbedingung angegeben, die in dem System gelten soll. Wir zeigen, wie durch eine solche Spezifikation ein sie implementierender endlicher Automat definiert ist und geben einen Algorithmus zu seiner Berechnung auf der Grundlage einer Fixpunkt-Iteration an.
Temporal stratifizierte Programme sind spezielle Logik-Programme auf der Grundlage einer linearen, temporalen Aussagenlogik, mit denen zustandsendliche reaktive Systeme spezifiziert werden können. Dabei wird die Umgebung eines zu implementierenden Steuerungsprogrammes durch eine Menge von PROLOG-ähnlichen Programmklauseln beschrieben; zusätzlich wird eine Sicherheitsbedingung angegeben, die in dem System gelten soll. Die Sprache ist so gestaltet, daß sie für resolutionsbasierte Verfahren zur Verifikation und Synthese von Steuerungsprogrammen geeignet ist. Wir zeigen, daß temporal stratifizierte Programme in ihrer Ausdrucksmächtigkeit endlichen Automaten gleichkommen.
Software development organizations measure their real-world processes, products, and resources to achieve the goal of improving their practices. Accurate and useful measurement relies on explicit models of the real-world processes, products, and resources. These explicit models assist with planning measurement, interpreting data, and assisting developers with their work. However, little work has been done on the joint use of measurem(int and process technologies. We hypothesize that it is possible to integrate measurement and process technologies in a way that supports automation of measurement-based feedback. Automated support for measurementbased feedback means that software developers and maintainers are provided with on-line, detailed information about their work. This type of automated support is expected to help software professionals gain intellectual control over their software projects. The dissertation offers three major contributions. First, an integrated measurement and
process modeling framework was constructed. This framework establishes the necessary foundation for integrating measurement and process technologies in a way that will permit automation. Second, a process-centered software engineering environment was developed to support measurement-based feedback. This system provides personnel with information about the tasks expected of them based on an integrated set of measurement and process views. Third, a set of assumptions and requirements about that system were examined in a controlled experiment. The experiment compared the use of different levels of automation to evaluate the acceptance and effectiveness of measurement-based feedback.
In this work we propose a set of term-rewriting techniques for modelling object-oriented computation. Based on symbolic variants of explicit substitutions calculi, we show how to deal with imperative statements like assignment and sequence in specifications in a pure declarative style. Under our model, computation with classes and objects becomes simply normal form calculation, exactly as it is the case in term-rewriting based languages (for instance the functional languages). We believe this kind of unification between functions and
objects is important because it provides plausible alternatives for using the term-rewriting theory as an engine for supporting the formal and mechanical reasoning about object-oriented specifications.
Visualization of large data sets, especially on small machines, requires advanced techniques in image processing and image generation. Our hybrid raytracer is capable of rendering volumetric and geometric data simultaneously, without loss of accuracy due to data conversion. Compound data sets, consisting of several types of data, are called "hybrid data sets". There is only one rendering pipeline to obtain loss-less and efficient visualization of hybrid data. Algorithms apply to both types of data. Optical material properties are stored in the same data base for both volumetric and geometric objects, and anti-aliasing methods appeal to both data types. Stereoscopic display routines have been added to obtain true three-dimensional visualization on various media, and animation features allow generation of recordable 3-D sequences.
Die dreidimensionale Darstellung hybrider Datensätze hat sich in den letzten Jahren als
ein wichtiger Teilbereich der wissenschaftlichen Visualisierung etabliert. Hybride Datensätze enthalten sowohl diskrete Volumendaten als auch durch geometrische Primitive
definierte Objekte. Bei der visuellen Verarbeitung einer gegebenen Szene spielen Schatteninformationen eine wichtige Rolle, indem sie die Beziehungen von Objekten untereinander verständlich machen. Wir beschreiben ein einfaches Verfahren zur Berechnung von Schatteninformation, das in ein bestehendes System zur Visualisierung hybrider Datensätze integriert wurde. An einem Beispiel aus der klinischen Anwendung werden die Ergebnisse illustriert.
The composition of Bézier curves and tensor product Bézier surfaces, polynomial as well as rational, is applied to exactly and explicitely represent trim curves of tensor product Bézier surfaces. Trimming curves are assumed to be defined as Bézier curves in surface parameter domain. A Bézier spline approximation of lower polynomial degree is built up as weil which is based on the exact trim curve representation in coordinate space.