05 Fakultät Informatik, Elektrotechnik und Informationstechnik
Permanent URI for this collectionhttps://elib.uni-stuttgart.de/handle/11682/6
Browse
42 results
Search Results
Item Open Access Fragments of first-order logic over infinite words(2009) Diekert, Volker; Kufleitner, ManfredWe give topological and algebraic characterizations as well as language theoretic descriptions of the following subclasses of first-order logic for omega-languages: Sigma2, FO2, the intersection of FO2 and Sigma2, and Delta2 (and by duality Pi2 and the intersection of FO2 and Pi2). These descriptions extend the respective results for finite words. In particular, we relate the above fragments to language classes of certain (unambiguous) polynomials. An immediate consequence is the decidability of the membership problem of these classes, but this was shown before by Wilke and Bojanczyk and is therefore not our main focus. The paper is about the interplay of algebraic, topological, and language theoretic properties.Item Open Access Reachability analysis of multithreaded software with asynchronous communication(2005) Bouajjani, Ahmed; Esparza, Javier; Schwoon, Stefan; Strejcek, JanWe 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.Item Open 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.Item Open 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.Item Open Access Existential and positive theories of equations in graph products(2001) Diekert, Volker; Lohrey, MarkusWe 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.Item Open Access Deriving bisimulation congruences in the DPO approach to graph rewriting. Long version(2004) Ehrig, Hartmut; König, BarbaraMotivated 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.Item Open Access Automatic synthesis of distributed transition systems(2006) Stefanescu, Alin; Esparza, Javier (Prof. Dr.)This thesis investigates the synthesis problem for two classes of distributed transition systems: synchronous products and asynchronous automata. The underlying structure of these models consist of local automata synchronizing on common actions. The synthesis problem discussed is as follows: Given a global specification as a transition system TS and a distribution pattern D, find a distributed transition system over D whose global state space is equivalent' to TS. As criteria for the correctness of the (distributed) implementation vs. the specification (i.e., their equivalence') we use: transition system isomorphism, language equivalence, and bisimilarity respectively. In particular, the synthesis of asynchronous automata modulo language equivalence is a notoriously hard problem solved by Zielonka at the end of the 80s. One of the motivations behind our work was to bring this theory closer to practical applications. From the theoretical point of view, we conduct a detailed analysis of the synthesis problem for both models of distributed systems, look at effective algorithmic approaches and draw a map of computational complexity results. E.g., we provide several matching lower and upper complexity bounds for the distributed implementability problem. From the practical perspective, we provide prototype implementations for most of the synthesis algorithms discussed in the thesis. Moreover, we offer assistance when a given specification is not distributable by trying to modify this specification such that distributed synthesis can be applied. By using several heuristics to overcome the classical state space explosion, we are able to automatically generate small distributed algorithms for problems such as mutual exclusion.Item Open Access XPASCAL - eine Erweiterung der Sprache Pascal mit exakter Arithmetik(1989) Lagally, KlausXPASCAL 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.Item Open Access Counterexample-guided abstraction refinement for the analysis of graph transformation systems(2006) König, Barbara; Kozioura, VitaliGraph transformation systems are a general specification language for systems with dynamically changing topologies, such as mobile and distributed systems. Although in the last few years several analysis and verification methods have been proposed for graph transformation systems, counterexample-guided abstraction refinement has not yet been studied in this setting. We propose a counterexample-guided abstraction refinement technique which is based on the over-approximation of graph transformation systems by Petri nets. We show that a spurious counterexample is caused by merging nodes during the approximation. We present a technique for identifying these merged nodes and splitting them using abstraction refinement, which removes the spurious run. The technique has been implemented in the Augur tool and experimental results are discussed.Item Open Access Makanin's algorithm for solving word equations with regular constraints(1998) Diekert, VolkerWe 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.