05 Fakultät Informatik, Elektrotechnik und Informationstechnik

Permanent URI for this collectionhttps://elib.uni-stuttgart.de/handle/11682/6

Browse

End date: 2004Institute: search.filters.UBSInstitut.Institut für Formale Methoden der Informatik

Search Results

Now showing 1 - 10 of 22
  • Thumbnail Image
    ItemOpen Access
    Computational and logical aspects of infinite monoids
    (2003) Lohrey, Markus; Diekert, Volker (Prof. Dr.)
    The present work contains a treatise of several computational and logical aspects of infinite monoids. The first chapter is devoted to the word problem for finitely generated monoids. In particular, the relationship between the the computational complexity of the word problem and the syntactical properties of monoid presentations is investigated. The second chapter studies Cayley-graphs of finitely generated monoids under a logical point of view. Cayley-graphs of groups play an important role in combinatorial group theory. We will study first-order and monadic second-order theories of Cayley-graphs for both groups and monoids. The third chapter deals with word equations over monoids. Using the graph product operation, which generalizes both the free and the direct product, we generalize the seminal decidability results of Makanin on free monoids and groups to larger classes of monoids.
  • Thumbnail Image
    ItemOpen Access
    Gleichungen mit regulären Randbedingungen über freien Gruppen
    (2000) Hagenah, Christian; Diekert, Volker (Prof. Dr.)
    Wir beweisen, daß das Erfüllbarkeitsproblem für Gleichungen mit regulären Randbedingungen über freien Gruppen PSPACE-vollständig ist. Wir zeigen auch, daß eine minimale Lösung einer solchen Gleichung höchstens eine doppelt exponentielle Länge hat und in 2-DEXPTIME berechnet werden kann. Wir reduzieren zuerst das Problem Gleichungen mit regulären Randbedingungen über einer freien Gruppen zu lösen auf das Problem Gleichungen mit regulären Randbedingungen über freien Monoiden mit einer Anti-Involution zu lösen. Anschließend stellen wir einen Algorithmus vor, der in PSPACE entscheidet, ob diese Gleichungen lösbar sind und einen Algorithmus, der in 2-DEXPTIME eine Lösung berechnet, wenn die Gleichung lösbar ist.
  • Thumbnail Image
    ItemOpen Access
    Existential and positive theories of equations in graph products
    (2001) Diekert, Volker; Lohrey, Markus
    We prove that the existential theory of equations with normalized rational constraints in a fixed graph product of finite monoids, free monoids, and free groups is PSPACE-complete. Under certain restrictions this result also holds if the graph product is part of the input. As the second main result we prove that the positive theory of equations with recognizable constraints in graph products of finite and free groups is decidable.
  • Thumbnail Image
    ItemOpen Access
    Deriving bisimulation congruences in the DPO approach to graph rewriting. Long version
    (2004) Ehrig, Hartmut; König, Barbara
    Motivated by recent work on the derivation of labelled transitions and bisimulation congruences from unlabelled reaction rules, we show how to solve this problem in the DPO (double-pushout) approach to graph rewriting. Unlike in previous approaches, we consider graphs as objects, instead of arrows, of the category under consideration. This allows us to present a very simple way of deriving labelled transitions (called rewriting steps with borrowed context) which smoothly integrates with the DPO approach, has a very constructive natureand requires only a minimum of category theory. The core part of this paper is the proof sketch that the bisimilarity based on rewriting with borrowed contexts is a congruence relation.
  • Thumbnail Image
    ItemOpen Access
    XPASCAL - eine Erweiterung der Sprache Pascal mit exakter Arithmetik
    (1989) Lagally, Klaus
    XPASCAL ist ein experimentelles Programmsystem zur Unterstützung exakter Berechnungen in arithmetischen Zahlkörpern, das derzeit in der Abteilung Betriebssoftware am Institut für Informatik der Universität Stuttgart entwickelt wird. Bisher haben daran neben dem Verfasser die Studenten G. Neusetzer, U. Schoppe, G. Wahl, Th. Schöbel und S. Robitschko mitgearbeitet. Der vorliegende Bericht soll die derzeitigen Zielvorstellungen und den Stand der Realisierung aufzeigen und zu Kommentaren, Änderungswünschen und Verbesserungsvorschlägen einladen.
  • Thumbnail Image
    ItemOpen Access
    Makanin's algorithm for solving word equations with regular constraints
    (1998) Diekert, Volker
    We give a self-contained proof of a fundamental result of Makanin (1977), which solves the satisfiability problem of equations with constants over free monoids. Our presentation of Makanin's algorithm is borrows Schulz (1992a), where Makanin's result is extended to the case where solutions are restricted by imposing regular constraints on the variables. This report appears (with minor modifications) as a chapter of the new book of M. Lothaire Algebraic Combinatorics on Words.
  • Thumbnail Image
    ItemOpen Access
    Analysis and verification of systems with dynamically evolving structure
    (2004) König, Barbara; Esparza, Javier (Prof. Dr.)
    This thesis is concerned with verification and analysis techniques for software systems characterized by dynamically evolving structure, such as dynamic creation and deletion of objects, mobility and variable topology. Examples for such systems are pointer structures, object-based systems and communication protocols in which the number of participants is not constant. The approach taken here is based on graph transformation systems, an intuitive and---at the same time---powerful formalism for the modelling of distributed and mobile systems. So far there exists comparatively little research concerning the verification of graph rewriting. We will---in the first part of this thesis---introduce graph transformations and give an overview of existing analysis and verification methods, with a focus on the verification of systems with dynamically evolving structure. Then we will describe three original lines of research: behavioural equivalences, type systems and approximation by Petri nets, all of them concerned with the analysis of graph transformation systems. The second part consists of eight refereed research papers treating the previously introduced analysis and verification techniques in depth.
  • Thumbnail Image
    ItemOpen Access
    Hierarchische Graphen zur Wegesuche
    (2000) Buchholz, Friedhelm; Claus, Volker (Prof. Dr.)
    In dieser Arbeit wird ein Zwei-Phasenmodell zur effizienten Entfernungsberechnung in gewichteten Graphen untersucht. Bekannte Anwendungsgebiete sind Verkehrsinformationssyteme, VLSI Design, Verteiltes Rechnen und geometrische und parallele Algorithmen. In einer Preprocessing-Phase wird zu einem Graphen ein Hierarchischer Graph (HG) konstruiert, der in der Online-Phase zur Entfernungsberechnung eingesetzt wird. Es werden die Laufzeit (T) der Preprocessing-Phase, die Groesse (S) des HG'en und die Laufzeit (Q) der Online-Phase untersucht. Zwei kontraere Modellierungsansaetze werden vorgestellt: Geeignete Knoten und ein rekursives Separationskonzept. Das Konzept mit Geeigneten Knoten wird auf Levelgraphen verallgemeinert und es wird gezeigt, dass die Berechnung einer minimalen Geeigneten Knotenmenge NP-vollstaendig ist. Die Approximation bzgl. der Groesse der Geeigneten Knotenmenge kann bis auf einen logarithmischen Faktor und bezueglich des Umgebungsabstands bis auf einen konstanten Faktor in polynomieller Laufzeit durchgefuehrt werden. Im Falle von planaren Graphen wird mittels eines erweiterten Separationskonzepts (Ideen von Lingas 1990 und von Didjev 1996 werden kombiniert) gezeigt, dass HG'en von fast linearer Groesse genuegen, um Q in O(n {1.5} log 3 n) zu gewaehrleisten. Dieses Resultat ist modulo logarithmischer Faktoren optimal. Ausserdem wird ein neuer Parameter 'Separatorweite' fuer Graphen eingefuehrt und es wird konstruktiv gezeigt, dass die Separatorweite unabhaengig von der Baumweite ist, aber hoechstens um einen logarithmischen Faktor von der Baumweite abweicht. Am Beispiel wird gezeigt, dass eine logarithmische Abweichung auftreten kann.
  • Thumbnail Image
    ItemOpen Access
    Endbericht der Projektgruppe Transportoptimierung
    (1998) Fleischmann, Jörg; Hermes, Lars; Spribille, Tobias
    Dieses Dokument ist die Fortsetzung des Zwischenberichts der Projektgruppe Transportoptimierung (TR-1996-06). Beide Berichte zusammen ergeben einen kontinuierlichen Überblick über die Arbeit der Projektgruppe von Oktober 1997 bis September 1998. Im Rahmen der Projektgruppe soll das Programm TROSS (TRansport-Organisation für Soziale Serviceanbieter) zur Verwaltung und Optimierung von sozialen Fahrdiensten entwickelt werden, das dann beim DRK in Stuttgart eingesetzt wird. Der Endbericht setzt dort an, wo der Zwischenbericht endet: Beim Entwurf. Teile des Entwurfs, die erst nach dem Zwischenbericht fertiggestellt wurden, oder deren Notwendigkeit sich gar erst während der Implementierungsphase ergab, sind hier festgehalten. Danach folgt der Bericht über die wichtigsten Aspekte der Projektphasen Implementierung und Test. Eine Übersicht über das entstandene Programm aus Programmierersicht sowie eine Bedienungsanleitung beendet die Beschreibung des entstandenen Systems. Abschließend wird der Ablauf des Projekts diskutiert und Anregungen für zukünftige Projektgruppen werden gegeben.
  • Thumbnail Image
    ItemOpen Access
    Complexity results for checking distributed implementability
    (2004) Heljanko, Keijo; Stefanescu, Alin
    We consider the distributed implementability problem as: Given a labelled transition system TS together with a distribution D of its actions over a set of processes, does there exist a distributed system over D such that its global transition system is equivalent' to TS? We consider the distributed system models of synchronous products of transition systems and Zielonka's asynchronous automata. In this paper we provide complexity bounds for the above problem with three interpretations of equivalent': as transition system isomorphism, as language equivalence, and as bisimilarity. In particular, we solve two problems left open in the literature. We also describe a logic programming implementation which complements the existing implementation for the synthesis of asynchronous automata initiated by the second author.