05 Fakultät Informatik, Elektrotechnik und Informationstechnik
Permanent URI for this collectionhttps://elib.uni-stuttgart.de/handle/11682/6
Browse
38 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 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 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.Item Open Access Efficient algorithms for alternating pushdown systems : application to certificate chain discovery with threshold subjects(2006) Suwimonteerabuth, Dejvuth; Schwoon, Stefan; Esparza, JavierMotivated by recent applications of pushdown systems to computer security problems, we present an efficient algorithm for the reachability problem of alternating pushdown systems. Although the algorithm is exponential, a careful analysis reveals that the exponent is usually small in typical applications. We show that the algorithm can be used to compute winning regions in pushdown games. In a second contribution, we observe that the algorithm runs in polynomial time for a certain subproblem, and show that the computation of certificate chains with threshold certificates in the SPKI/SDSI authorization framework can be reduced to this subproblem. We present a detailed complexity analysis of the algorithm and its application, and report on experimental results obtained with a prototype implementation.Item Open Access First-order fragments with successor over infinite words(2010) Kallas, Jakub; Kufleitner, Manfred; Lauser, AlexanderWe consider fragments of first-order logic and as models we allow finite andinfinite words simultaneously. The only binary relations apart from equalityare order comparison < and the successor predicate +1. We givecharacterizations of the fragments Sigma2 = Sigma2[<,+1] and FO2 = FO2[<,+1] interms of algebraic and topological properties. To this end we introduce thefactor topology over infinite words. It turns out that a language L is in theintersection of FO2 and Sigma2 if and only if L is the interior of an FO2language. Symmetrically, a language is in the intersection of FO2 and Pi2 ifand only if it is the topological closure of an FO2 language. The fragmentDelta2, which by definition is the intersection Sigma2 and Pi2 contains exactlythe clopen languages in FO2. In particular, over infinite words Delta2 is astrict subclass of FO2. Our characterizations yield decidability of themembership problem for all these fragments over finite and infinite words; andas a corollary we also obtain decidability for infinite words. Moreover, wegive a new decidable algebraic characterization of dot-depth 3/2 over finitewords. Decidability of dot-depth 3/2 over finite words was first shown by Glaßer andSchmitz in STACS 2000, and decidability of the membership problem for FO2 overinfinite words was shown 1998 by Wilke in his habilitation thesis whereasdecidability of Sigma2 over infinite words was not known before.Item Open Access Infinite state model checking of propositional dynamic logics(2006) Göller, Stefan; Lohrey, MarkusModel-checking problems for propositional dynamic logic (PDL) and its extension PDL$^\cap$ (which includes the intersection operator on programs) over various classes of infinite state systems (BPP, BPA, pushdown systems, prefix-recognizable systems) are studied. Precise upper and lower bounds are shown for the data/expression/combined complexity of these model-checking problems.