05 Fakultät Informatik, Elektrotechnik und Informationstechnik

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

Browse

Filters

Settings

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

Search Results

Now showing 1 - 10 of 30
  • Thumbnail Image
    ItemOpen Access
    Reachability analysis of multithreaded software with asynchronous communication
    (2005) Bouajjani, Ahmed; Esparza, Javier; Schwoon, Stefan; Strejcek, Jan
    We introduce asynchronous dynamic pushdown networks (ADPN), a new model for multithreaded programs in which pushdown systems communicate via shared memory. ADPN generalizes both CPS (concurrent pushdown systems) and DPN (dynamic pushdown networks). We show that ADPN exhibit several advantages as a program model. Since the reachability problem for ADPN is undecidable even in the case without dynamic creation of processes, we address the bounded reachability problem, which considers only those computation sequences where the (index of the) thread accessing the shared memory is changed at most a fixed given number of times. We provide efficient algorithms for both forward and backward reachability analysis. The algorithms are based on automata techniques for symbolic representation of sets of configurations.
  • 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
    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
    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
    A note on on-the-fly verification algorithms
    (2004) Schwoon, Stefan; Esparza, Javier
    The automata-theoretic approach to verification of LTL relies on an algorithm for finding accepting cycles in the product of the system and a Büchi automaton for the negation of the formula. Explicit-state model checkers typically construct the product space "on the fly" and explore the states using depth-first search. We survey algorithms proposed for this purpose and propose two improved algorithms, one based on nested DFS, the other on strongly connected components. We compare these algorithms both theoretically and experimentally and determine cases where both algorithms can be useful.
  • Thumbnail Image
    ItemOpen Access
    Abschlußbericht der Projektgruppe Evolutionäre Algorithmen
    (1997) Großmann, Matthias; Leonhardi, Alexander; Schmidt, Thomas
    Viele in der Praxis interessante Optimierungsrobleme sind NP-hart. Da kein Algorithmus bekannt ist, der ein Optimum für solche Probleme mit geringerem als exponentiellem Aufwand findet, sucht man, ein Optimum mit Heuristiken möglicht gut anzunähern. Zu diesen gehören auch die Evolutionären Algorithmen. Ziel der Projektgruppe EVA war die Entwicklung einer Experimentierplattform für Evolutionäre Algorithmen, die die Implementierung und empirische Untersuchung dieser Algorithmen erleichtert. Besonderer Wert wurde daher auf möglichst große Unabhängigkeit der Algorithmen vom Problem gelegt. Der Endbericht der Projektgruppe enthält nach einer Einführung den Entwurf von GENOM, die Beschreibung der Implementierung sowie Hinweise zur Bedienung und zu Erweiterungsmöglichkeiten.
  • 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
    Reguläre Häufigkeitsberechnungen
    (2005) Austinat, Holger; Diekert, Volker (Prof. Dr.)
    Die vorliegende Arbeit beschäftigt sich mit Häufigkeitsberechnungen, einem rekursionstheoretischen Begriff, der in den 60er Jahren von Rose eingeführt wurde. Eine Funktion f ist berechenbar mit Frequenz m/n, wenn es einen Algorithmus gibt, der für je n verschiedene Eingaben n Ausgabewerte berechnet, von denen mindestens m mit den zugehörigen Funktionswerten von f übereinstimmen. Eine erste natürliche Fragestellung war: gibt es nicht-berechenbare Funktionen, die mit einer Frequenz nahe 1 berechnet werden können? Trakhtenbrot beantwortete diese Frage 1963 negativ, indem er zeigte, dass eine Funktion mit Frequenz echt größer als 1/2 bereits berechenbar im herkömmlichen Sinne ist. Andererseits gibt es überabzählbar viele Funktionen, die sich mit Frequenz 1/2 berechnen lassen. Also ist dieses Ergebnis optimal. Die Forschung auf diesem Gebiet intensivierte sich daraufhin: Wissenschaftler wie Dëgtev, Kinber und Trakhtenbrot selbst (in den 70er und 80er Jahren) und Beigel, Gasarch, Hinrichs, Kummer, Stephan, Tantau und Wechsung (ab den 90er Jahren) beschäftigten sich mit verschiedenen Aspekten von Häufigkeitsberechnungen und verwandten Berechenbarkeitsbegriffen. In der vorliegenden Arbeit beschäftigen wir uns vorwiegend mit regulären Häufigkeitsberechnungen, also solchen, die von endlichen Automaten vorgenommen werden können. Kinber untersuchte diesen Aspekt als erster im Jahre 1976 und behauptete, dass sich Trakhtenbrots Resultat auf endliche Automaten überträgt. Sein folgerte dies aus einem allgemeineren Resultats über separierbare Sprachen, das sich allerdings als falsch herausstellte (ein Gegenbeispiel wurde 2002 von Tantau angegeben). (Zwei disjunkte Sprachen A und B heißen separierbar, wenn ein Algorithmus alle Wörter aus A akzeptiert und alle Wörter aus B ablehnt). Die Frage, ob das Analogon von Trakhtenbrots Resultat für endliche Automaten gilt, stellte sich also von neuem. Diese Dissertation enthält folgende Ergebnisse. In Kapitel 2 geben wir zwei Beweise für Trakhtenbrots Resultat an. Zunächst präsentieren wir seinen Originalbeweis, um dann einen neuen kombinatorischen Beweis zu geben, der einen großen Vorteil besitzt: er erlaubt die Übertragung des Ergebnisses auf endliche Automaten. Zwei kleinere Resultate beschließen dieses Kapitel: der Nachweis, dass es überabzählbar viele nicht häufigkeitsberechenbare Sprachen gibt, und eine Darstellung des Zusammenhangs von Häufigkeitsberechnungen und sog. mulit-selektiven Mengen. In Kapitel 3 arbeiten wir den Fehler in Kinbers Beweis über separierbare Sprachen heraus und geben ein konkretes Gegenbeispiel an. Dann untersuchen wir die Separierbarkeit von sog. Pfad- und Anti-Pfadsprachen, die wie folgt definiert sind: sei alpha ein unendliches Wort über dem Alphabet { 0, 1 }; dann ist A(alpha) die Menge der endlichen Präfixe von alpha, und B(alpha) die Menge der Wörter von A(alpha), bei denen das letzte Bit negiert wurde. Wir zeigen, dass A(alpha) und B(alpha) genau dann separiert werden können, wenn die 1-Positionen von alpha berechnet werden können. Andererseits gibt es überabzählbar viele alpha, für die A(alpha) und B(alpha) mit Frequenz 1/2 berechnet werden können. Wenn (ab drei Eingaben) nur ein Fehler zugelassen ist, dann sind A(alpha) und B(alpha) bereits rekursiv. Dieses Ergebnis überträgt sich auch auf endliche Automaten. Zum Abschluss dieses Kapitels zeigen wir, dass sich Kinbers Vermutung (dass Trakhtenbrots Resultat auch für Sprachen gilt, die durch endliche Automaten separiert werden können) nicht retten lässt: für jede Konstante q < 1 gibt es Werte 1 <= m < n mit m/n > q und ein alpha derart, dass A(alpha) und B(alpha) durch endliche Automaten mit Frequenz m/n separiert werden können, jedoch nicht rekursiv separierbar sind. In Kapitel 4 untersuchen wir verschiedene Aspekte regulärer Häufigkeitsberechnungen. Wir zeigen zunächst, dass sich Trakhtenbrots Resultat auf endliche Automaten überträgt, indem wir den neuen Beweis aus Kapitel 2 nochmals genauer betrachten. Anschließend zeigen wir, dass aperiodische Automaten, die Häufigkeitsberechnungen durchführen, nur aperiodische reguläre Sprachen berechnen können (aperiodische Sprachen entsprechen sternfreien Sprachen). Dann beweisen wir ein sog. Iterationskriterium, das vergleichbar mit dem bekannten Pumping-Lemma für reguläre Sprachen ist und uns für viele konkrete Beispielsprachen den Nachweis erlaubt, dass diese nicht häufigkeitsberechenbar sind. Im letzten Teil untersuchen wir dann Abschlusseigenschaften der Klasse der regulär häufigkeitsberechenbaren Sprachen: wir zeigen, dass sie eine boolesche Algebra bilden, jedoch nicht unter Spiegelung abgeschlossen sind. Darüberhinaus ist die Vereinigung zweier Sprachen, die mit Frequenz 1/n erkennbar sind, in der Regel nicht 1/n-erkennbar. Wir beweisen eine untere Schranke, die sehr nah an der besten bekannten oberen Schranke liegt.
  • 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
    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.