Man benutzt Wort- und Termersetzungssysteme als Berechnungsmodell. Dabei fordert man typischerweise, dass das System terminiert, damit die Rechnungen auch Ergebnisse liefern. Ist das Gegenteil der Fall, möchte man gern wissen, warum. Wir stellen einige automatisierte Methoden vor, mit denen man unendliche Ableitungen findet. Insbesondere geht es um unendliche Ableitungen ohne Schleifen.
Following the MSO graph transduction approach of Courcelle, functions
on graphs can be described using families of MSO formulas with one and
two free variables. If the graphs are restricted to trees, then we
obtain the MSO definable tree translations. They form a natural class of
translations with many good properties (such as closure under sequential
composition). We show that the equivalence problem for such MSO tree
transducers is decidable. In fact, even for MSO graph-to-tree transducers
it is decidable whether they are equivalent on a context-free set of
graphs. The proof is based on the fact that images of context-free
graph languages under MSO translations are Parikh (i.e., their
Parikh vectors form a semi-linear set). We do not not yet know the complexity
of our decision procedure. For tree-to-tree translations obtained
by unfolding the output dags of MSO definable tree-to-dag translations
it remains open whether equivalence is decidable (this coincides
with the equivalence problem for attribute grammars).
If time permits, then we also mention recent results on equivalence of
deterministic top-down tree transducers; for total transducers, equivalence
can be decided in polynomial time.
Based on joint work with
Joost Engelfriet and Helmut Seidl, respectively.
In this talk we introduce the McLain groups and present certain results on perfect subgroup structure of these groups. We determine the structure of McLain groups as semi-direct products and as generations of perfect proper subgroups which have many interesting properties. We also construct certain groups using McLain groups' non-co-Hopfian structures and give an approach to figure out the subgroups of these groups as reflections of topological ideas.
In the talk we will characterize the recursion theoretic complexity of the existence of an Euler path in a recursive/automatic graph. We will prove that the existence of an Euler path in a recursive graph is complete for the class DΣ03. This class consists of all set differences of Σ03 sets. The same problem for highly recursive graphs as well as automatic graphs is shown to be Π02-complete. Moreover, the arithmetic level for bounding the number of ends in an automatic/recursive graph as well as computing the number of infinite paths in an automatic/recursive finitely branching tree is determined.
In meinem Vortrag werde ich die Logik μ-ICPDLNom einführen. Sie erweitert den modalen μ-Kalkül von Kozen und ICPDL (Propositionale Dynamische Logik mit Durchschnitt und Umkehrung von Programmen) und erlaubt zusätzlich die Verwendung von Konstanten, sogenannten Nominalen. Modelle von μ-ICPDLNom-Formeln sind Kripke-Strukturen. In meinem Vortag werde ich mich auf die Modelleigenschaft von μ-ICPDLNom konzentrieren. Es wird ein Art Entfaltungsoperator auf Kripke-Strukturen definiert, der μ-ICPDLNom-Theorien erhält. Daraus kann abgeleitet werden, dass jede erfüllbare μ-ICPDLNom-Formel die höchstens k verschiedene Nominale enthält ein abzählbares Modell der Baumweite höchstens k+2 besitzt. Mit diesen Überlegungen und einer Reduktion auf das Leerheitsproblem für alternierende Zweiweg-Automaten auf unendlichen Bäumen kann gezeigt werden, dass Erfüllbarkeit von μ-ICPDLNom vollständig für deterministische zweifach exponentielle Zeit ist. Dies ist eine gemeinsame Arbeit mit Markus Lohrey und verallgemeinert eine Arbeit gemeinsam mit Markus Lohrey und Carsten Lutz (PDL with Intersection is 2EXP-complete, FOSSACS 2007).
TREEBAG ist ein Programm, das die Erzeugung von Zeichenketten, Bäumen, Bildern und anderen Objekten mithilfe von Baumgrammatiken und Baumtransformationen erlaubt. Die Idee ist einfach und spätestens seit Mezeis und Wrights berühmten Artikel von 1967 wohlbekannt: Die Ausgabebäume von Baumgrammatiken und Baumtransformationen werden von geeigneten Algebren interpretiert, um nicht nur Bäume erzeugen zu können, sondern im Prinzip beliebige Objekte. Zu diesem Zweck stellt TREEBAG vier Grundtypen von Komponenten zur Verfügung, nämlich Baumgrammatiken, Baumtransformationen, Algebren und Displays, wobei Letztere der geeigneten Präsentation der resultierenden Objekte dienen. Bei der Entwicklung des Systems spielte die leichte Erweiterbarkeit durch neue Typen von Baumgrammatiken, Baumtransformationen, Algebren und Displays eine entscheidende Rolle. Im Vortrag werde ich TREEBAG vorstellen, Beispiele zeigen und Ideen für ein Nachfolgersystem diskutieren.
Wir betrachten eine gewichtete Version von Petri-Netzen, in dem die Transitionen eine natürliche Zahl zugewiesen bekommen. Das Gewicht einer Transition wird als Kosten für das Feuern der Transition interpretiert. Weiterhin unterscheiden wir zwischen einem Modell, in dem die Kosten einer Berechnungsfolge durch einfaches Aufaddieren der Gewichte der beteiligten Transitionen berechnet werden, sowie einem Modell, in dem die Kosten zusätzlich linear von der Anzahl der Tokens in einer Markierung abhängen. Wir untersuchen das minimale-Kosten-Überdeckungsproblem: was sind die minimalen Kosten, um von einer gegebenen endlichen Menge von Anfangsmarkierungen zu einer nach oben abgeschlossenen Menge von Finalmarkierungen zu gelangen? Im Vortrag werde ich Algorithmen zur Lösung des Problems vorstellen, die die Ausgangsbasis für die Lösung des gleichen Problems einer gewichteten Version von Zeit-Petri-Netzen stellen (wird in einem späteren Vortrag vorgestellt).
Wir definieren einen gewichteten μ-Kalkül auf endlichen und unendlichen Wörtern. Dieser μ-Kalkül verwendet keine Konjunktion und die Gewichte stammen aus Halbringen mit gewissen Vollständigkeits- und Stetigkeitseigenschaften. Für eine Reihe gebräuchlicher Halbringe wie distributive vollständige Verbände, den tropischen und den probabilistischen Halbring zeigen wir, dass die Ausdrucksstärke des konjunktionslosen gewichteten μ-Kalkül mit der Klasse der omega-rationalen formalen Potenzreihen übereinstimmt.
Wir untersuchen die Gruppe aller durch eine Translation
beschränkten Ordnungsautomorphismen der reellen Zahlen.
Diese bilden eine sog. unitäre Verbandsgruppe, die
auf Grund ihrer Verbindungen zu mv-Algebren unabhängiges
Interesse genießt. Wie bekannt, hat die Gruppe aller
Ordnungsautomorphismen von R genau drei nichttriviale
echte Normalteiler. Wir zeigen nun, dass obige Gruppe
2c Normalteiler hat, wobei c die Mächtigkeit des
Kontinuums ist. Wir geben eine vollständige Chrakterisierung
des Normalteilerverbandes an.
M. Droste, W.C. Holland: Normal subgroups of BuAut(Ω),
Appl. Categor. Structures 15 (2007), 153-162.
Nested words, a model for recursive programs proposed by Alur and Madhusudan, have only recently gained much interest. In this talk we introduce quantitative extensions and study nested word series which assign to nested words elements of a semiring. We show that regular nested word series coincide with series definable in weighted logics as introduced by Droste and Gastin. In order to do so, we establish a connection between nested words and series-parallel-biposets. Applying the result, we obtain a characterization of algebraic formal power series in terms of weighted logic. This generalizes a result of Lautemann, Schwentick and Thérien.
In recent years there has been a growing interest in expanding decision algorithms to allow for explanation - and correction - of properties holding in a Knowledge Base (KB). If the decision procedure in hand explicitely uses elements in the KB, then this task is as simple as tracking the elements that were used to obtain the result. Unfortunately, automata-based decision procedures use KBs implicitely. In this talk, we show how weighted automata can be used for computing a propositional formula from which the desired explanations can be deduced.
We investigate the relation between the theory of the iterations in the sense of Shelah-Stupp and of Muchnik, resp., and the theory of the base structure for several logics. These logics are obtained from the restriction of set quantification in monadic second order logic to certain subsets like, e.g., finite sets, chains, and finite unions of chains. We show that these theories of the Shelah-Stupp iteration can be reduced to corresponding theories of the base structure. This fails for Muchnik's iteration.
Gemeinsame Arbeit mit Adam Koprowski (TU Eindhoven)
Ein Ersetzungssystem terminiert,
wenn es keine unendlich langen Berechnungen gestattet.
Wir interessieren uns für maschinelle Terminationsbeweise.
Ein wichtiges Beweisverfahren ist Interpretation
in eine monotone Algebra. Wir betrachten Interpretationen
durch gewichtete Baumautomaten. Als Gewichte verwenden wir
(a) natürliche Zahlen N mit Standard-Operationen (plus, mal),
(b) den arktischen Halbring (-infinity + N) mit (max, plus),
(c) den vollen arktischen Halbring (-infinity + Z).
Die Verfahren (a) und (b - bisher nur für Wortsersetzung)
werden seit 2006 bzw. 2007 von mehreren erfolgreichen Teilnehmern
der Termination Competitions
benutzt;
die Erweiterung von (b) für Termersetzung und (c) sind neu.
Im Vortrag diskutieren wir Korrektheit, Implementierung und formale Verifikation sowie eine Verbindung zum Beschränktheitsproblem für tropische (min,plus) Automaten.
Literatur:
Jörg Endrullis, Johannes Waldmann and Hans Zantema:
Matrix Interpretations for Proving Termination of Term Rewriting;
IJCAR 2006, JAR 2007.
Adam Koprowski and Hans Zantema:
Certification of Proving Termination of Term Rewriting
by Matrix Interpretations;
SOFSEM 2008.
Johannes Waldmann:
Weighted Automata for Proving Termination of String Rewriting;
WATA 2006, JALC 2007.
Automatische Graphen sind gegeben durch zwei endliche Automaten, die die Menge der Knoten bzw. die Menge der Kanten erkennen (hierfür wird ein synchroner Zweiband-Automat verwendet). Gefragt wird, wie sich graphtheoretische Eigenschaften in den Automaten widerspiegeln. Dabei zeigen wir, dass die Existenz eines unendlichen Hamiltonpfades Σ-1-1-vollständig ist, hingegen ist die Existenz einer unendlichen Clique entscheidbar - diese beiden Probleme sind für rekursive Graphen (d.h. wenn man Turingmaschinen an Stelle der endlichen Automaten zulässt) Σ-1-1-vollständig.
Wir betrachten eine komprimierte Variante des Wortproblems
in endlich erzeugten Gruppen, bei dem Eingabewörter durch
kontextfreie Grammatiken, die genau
ein Wort erzeugen (sogenannte Straight-Line Programme),
repräsentiert werden. Es wird gezeigt, dass die Komplexität
dieses komprimierten Wortproblems unter endlichen Erweiterungen
und freien Produkten erhalten wird. Für Graphgruppen
(frei partiell kommutative Gruppen) wird ein
Polynomialzeitalgorithmus für das komprimierte
Wortproblem angegeben. Wir werden diese Resultate auf
das (klassische, d.h. unkomprimierte) Wortproblem von
gewissen Gruppenerweiterungen und Automorphismengruppen
anwenden. Unter anderem ergibt sich ein Polynomialzeitalgorithmus
für das Wortproblem der Automorphismengruppe einer freien
Gruppe, was ein offenes Problem von Kapovich, Miasnikov, Schupp
und Shpilrain löst.
(gemeinsame Arbeit mit Saul Schleimer, Rutgers University)
Wir untersuchen eine bidirektionale Propositionale Dynamische Logik (PDL) auf so genannten Message Sequence Charts (MSCs), die Systeme mit Nachrichten-Austausch modellieren. Diese Logik erweitert frühere temporale Logiken. Mit dieser multi-modalen Logik können Eigenschaften sowohl in der Zukunft wie in der Vergangenheit eines Ereignisses ausgedrückt werden. Pfadausdrücke erweitern die Ausdrucksstärke des klassischen UNTIL-Operators. Jede Formel wird in eine äquivalente kommunizierende endliche Maschine (CFM) von exponentieller Größe übersetzt. Dieses Synthese-Problem lösen wir in voller Allgemeinheit, also auch für MSCs mit unbeschränkten Kanälen. Das Model-Checking-Problem für CFMs und HMSCs gegenüber Formeln aus PDL kann für existentiell beschränkte MSCs in PSPACE gelöst werden. Weiterhin wird gezeigt, dass CFMs nicht ausdrucksstark genug für PDL mit Durchschnitt sind. Dieses ist eine gemeinsame Arbeit mit Benedikt Bollig und Dietrich Kuske.
Chu spaces consider of a set of objects, a set of
attributes or properties, and a satisfaction relation
between objects and attributes. Many mathematical
structures including topological spaces, partial orders
and distributive lattices, can be modeled as Chu spaces.
In theoretical computer science, they can be used to
obtain models of linear logic and models for concurrent
processes.
We will investigate:
In Strukturfragen zu unendlichen Gruppen ist die Kofinalität ein wichtiges Konzept. Grob gesprochen gibt sie an, wie gut sich die Gruppe durch eine Kette von, z.B., Untergruppen approximieren lässt. Eng damit zusammen hängt eine relativ junge "Erfindung", nämlich die Bergman-Eigenschaft. Eine Gruppe mit dieser Eigenschaft hat ausschließlich "besonders große" Erzeugendensysteme. Die Bergman-Eigenschaft ist für eine Reihe von Permutationsgruppen verifiziert worden. Ich gebe einen Einblick in gängige und auch neue Beweismethoden; die letzteren haben wir benutzt, um zu zeigen, dass gewisse klassische Gruppen von maßerhaltenden Transformationen des Einheitsintervalls die Bergman-Eigenschaft haben.
Propositional Dynamic Logic (PDL), von Fischer und Ladner 1979 eingeführt, ist eine Erweiterung von Modallogik, die es erlaubt über reguläre Ausführungen von Programmen zu sprechen. Modelle von PDL sind Transitionssysteme. Eine wichtige algorithmische Fragestellung ist das Erfüllbarkeitsproblem, d.h. ob eine gegebene Formel ein Modell besitzt. Für PDL ist die Komplexität des Erfüllbarkeitsproblems schon lange bekannt - PDL ist vollständig für deterministisch exponentielle Zeit. In meinem Vortrag werde ich über die Komplexität des Erfüllbarkeitsproblems von ICPDL sprechen. ICPDL ist eine interessante Erweiterung von PDL, die im Gegensatz zu PDL weder die Baummodell- noch die endliche Modelleigenschaft besitzt und sowohl den Durschschnitt als auch die Umkehrung von Programmen erlaubt.
Ich werde zeigen, daß Erfüllbarkeit für ICPDL vollständig für deterministisch zweifach exponentielle Zeit ist, was die bisher bekannte nichtelementare obere Schranke von Lutz verbessert. Dies ist eine gemeinsame Arbeit mit Markus Lohrey und Carsten Lutz.