Forschungsseminar Theoretische Informatik

Wintersemester 2011/12

5.10.2011, 14:15 Uhr, Johannisgasse 26, 4-42
Yago Antolín Pichel (Southampton):
Tits alternatives for graph products

I will report some recent results in a ongoing work with Ashot Minasyan. We will discuss various types of Tits Alternative for finitely generated subgroups and prove that, under some natural conditions, the graph product of groups satisfies a given type of Tits Alternative if and only if each vertex group satisfies this alternative.

Sommersemester 2011

21.9.2011, 14:15 Uhr, Johannisgasse 26, 4-42
Markus Lohrey (Universität Leipzig):
Isomorphism of regular trees and words
(joint work with Christian Mathissen)

The computational complexity of the isomorphism problem for regular trees, regular linear orders, and regular words is analyzed. A tree is regular if it is isomorphic to the prefix order on a regular language. In case regular languages are represented by NFAs (DFAs), the isomorphism problem for regular trees turns out to be EXPTIME-complete (resp. P-complete). In case the input automata are acyclic NFAs (acyclic DFAs), the corresponding trees are (succinctly represented) finite trees, and the isomorphism problem turns out to be PSPACE-complete (resp. P-complete). A linear order is regular if it is isomorphic to the lexicographic order on a regular language. A polynomial time algorithm for the isomorphism problem for regular linear orders (and even regular words, which generalize the latter) given by DFAs is presented. This solves an open problem by Esik and Bloom.

31.8.2011, 14:15 Uhr, Johannisgasse 26, 4-42
Alexander Kartzow (Universität Leipzig):
A Pumping Lemma for Collapsible Pushdown Graphs of Level 2

We give a brief introduction to the hierarchy of collapsible pushdown graphs. In the last years this hierarchy has gained a lot of attention due to its connections to the verification of higher-order functional programs. Even though there are a lot of "model checking" results, i.e., results concerning decidability of certain logics on these graphs, we lack a theory on the structure of these graphs. The pumping lemma that we present in this talk is one of the few tools for disproving membership of a graph in the second level of the collapsible pushdown hierarchy.

Wintersemester 2010/11

19.1.2011, 15:00 Uhr, Johannisgasse 26, 4-42
Siegfried Gottwald (Universität Leipzig):
Lokale Endlichkeit in t-Norm basierten Bimonoiden und anderen t-Norm basierten Strukturen

This paper discusses the property of local finiteness for t-norm monoids and extensions of them. The focus is (i) on t-norm bimonoids, which are of interest in the context of weighted automata, (ii) on those extensions of t-norm monoids which are reducts of t-algebras, i.e. of the basic semantic entities for the (fuzzy) logics of left-continuous and of continuous t-norms, and (iii) on extensions of t-norm monoids with their residuation based standard negations. The paper introduces also a kind of relativized local finiteness.

5.1.2011, 15:15 Uhr, Johannisgasse 26, 4-42
Alexander Kartzow (TU Darmstadt):
Ramseys Styling-Tipps für (baum)automatische Strukturen - wie man mit Kämmen Ketten findet

Wir zeigen die Entscheidbarkeit der FO(Ram)-Theorie aller baumautomatischer Strukturen. FO(Ram) ist die Erweiterung der Logik erster Stufe um Ramseyquantoren. Eine Struktur S erfüllt eine Formel Ram x_1, ... x_n &phi, wenn es eine unendliche Teilmenge M von S gibt, so dass alle n-Tupel aus paarweise verschiedenen Elementen von M die Formel &phi erfüllen. Rubin zeigte die Entscheidbarkeit von FO(Ram) auf wortautomatischen Strukturen unter Benutzung des Konzepts der Wortkämme (eine Form der Codierung unendlich vieler endlicher Wörter in einem unendlichen Wort). Wir führen das Konzept eines Baumkamms ein und zeigen, wie man damit FO(Ram) auf baumautomatischen Strukturen entscheiden kann. Diese Technik kann auch verwendet werden um die Existenz unendlicher Ketten in partiellen Ordnungen zu entscheiden. Mithilfe dieser Resultate ist z.B. entscheidbar, ob eine gegebene definierbare Ordnung eine Quasiwohlordnung ist.

3.11.2010, 15:15 Uhr, Johannisgasse 26, 4-42
Vitaly Perevoshchikov (Universität Leipzig):
Probabilistische Omega-Automaten

Wir besprechen die wichtigsten Ergebnisse der Theorie probabilistischer Omega-Automaten über unendlichen Wörtern. Es wurde bewiesen, dass die Klasse der von probabilistischen Büchi-Automaten (PBA) erkennbaren Sprachen unter Komplement abgeschlossen ist. Obwohl das Leerheitsproblem für PBA nicht entscheidbar ist, kann gezeigt werden, dass die Leerheit für einen PBA mit fast sicherer Semantik entschieden werden kann. PBA sind ausdrucksstärker als nichtdeterministische Omega-Automaten. Außerdem kann die Unterklasse der PBA bestimmt werden, deren erkannte Sprachklasse mit der Klasse der omega-regulären Sprachen übereinstimmt.

27.10.2010, 15:15 Uhr, Johannisgasse 26, 4-42
Cris Calude (University of Auckland):
Is quantum randomness pseudo-randomness?

We discuss theoretical results and experimental evidence showing that quantum randomness certified by value indefiniteness is strongly incomputable, i.e. not pseudo-randomness.

Sommersemester 2010

14.7.2010, 15:15 Uhr, Johannisgasse 26, 4-42
Ingmar Meinecke (Universität Leipzig):
Regular Expressions on Average and in the Long Run

Quantitative aspects of systems like consumption of resources, output of goods, or reliability can be modeled by weighted automata. Recently, objectives like the average cost or the longtime peak power consumption of a system have been modeled by weighted automata which are not semiring weighted anymore. Instead, operations like limit superior, limit average, or discounting are used to determine the behavior of these automata. Here, we introduce a new class of weight structures subsuming a range of these models as well as semirings. Our main result shows that such weighted automata and Kleene-type regular expressions are expressively equivalent both for finite and infinite words.

This is joint work with Manfred Droste.

15.6.2010, 9:15 Uhr, Johannisgasse 26, 4-42
Jiamou Liu (University of Auckland und Universität Leipzig):
Computable Categoricity of Graphs with Finite Components

A graph is computable if its set of nodes and edge relation are computable sets. A computable graph is computably categorical if any two computable presentations of the graph are computably isomorphic. We focus on the class of computably categorical graphs. In particular, we investigate the strongly locally finite graphs: graphs all of whose components are finite. In this talk we discuss the following results: (1) We present a necessary and sufficient condition for certain classes of strongly locally finite graphs to be computably categorical. (2) Whenever there exists an infinite Δ ₂⁰-set of components that can be properly embedded into infinitely many components of the graph, the graph is not computably categorical. (3) There exists a strongly locally finite computably categorical graph with a infinite chain of properly embedded components.

9.6.2010, 15:15 Uhr, Johannisgasse 26, 4-42
Markus Lohrey ( Universität Leipzig):
Branching time model checking of one-counter processes

One-counter processes are pushdown processes which operate only on a unary stack alphabet. In this talk, I will survey recent progress on the complexity of various model checking problems over one-counter processes. The main focus will be on the temporal logic CTL and its fragment EF. It turns out that CTL model checking over one-counter processes is PSPACE-complete, where the lower bound already holds (i) for a fixed one-counter process (expression complexity) and (ii) for a fixed CTL formula (data complexity). The proof of the second result uses two interesting techniques from computational complexity theory: (i) Converting a natural number from Chinese remainder representation into binary representation is in logspace-uniform NC1 and (ii) PSPACE is AC0-serializable. For the CTL fragment EF we obtain complexity results for the complexity class P^NP.

This is joint work with Stefan Göller.

26.5.2010, 15:15 Uhr, Johannisgasse 26, 4-42
Manfred Droste ( Universität Leipzig):
Random constructions of countable abelian p-groups

By Ulm's theorem, countable reduced abelian p-groups are characterized, uniquely up to isomorphism, by their Ulm invariants. Given a sequence f of Ulm invariants, we provide a probabilistic construction of a countable abelian p-group G_f, having the set of natural numbers as its domain, with Ulm invariants less or equal to f. We then show that with probability 1, G_f has precisely f as its sequence of Ulm invariants. This establishes the existence part of Ulm's theorem in a probabilistic way. We also develop new results for valuated abelian p-groups which are essential for our construction.

Joint work with Rüdiger Göbel (Essen)

19.5.2010, 15:15 Uhr, Johannisgasse 26, 4-42
Christian Mathissen ( Universität Leipzig):
Compressed Conjugacy and the Word Problem for Outer Automorphism Groups of Graph Groups

Similar to a trace monoid, a graph group is given by a finite undirected graph (G,I), where G is the set of generators and every edge (a,b) in I gives rise to a commutation relation ab=ba. We study the conjugacy problem, i.e. the decision problem whether two given words u,v over G represent conjugated elements in the graph group. We also study an extension, the so-called simultaneous conjugacy problem. We show that for graph groups the conjugacy problem as well as a restricted version of the simultaneous conjugacy problem can be solved in polynomial time even if input words are represented in a compressed form. As a consequence it follows that the word problem for the outer automorphism group of a graph group can be solved in polynomial time.

(Joint work with Niko Haubold and Markus Lohrey)

11.5.2010, 9:30 Uhr, Johannisgasse 26, 4-42
Martin Huschenbett (Universität Leipzig):
A Kleene-Schützenberger theorem for trace series over strong bimonoids

We study weighted trace automata with weights in strong bimonoids. Traces are a generalization of words that allow to model concurrency and strong bimonoids are algebraic structures that can be regarded as "semirings without distributivity", e.g. non-distributive lattices. We show that if both operations of the bimonoid are locally finite the classes of recognizable and mc-rational trace series coincide and, in general, are properly contained in the class of c-rational series. We further prove the coincidence of all three classes under the additional assumption of commutativity and idempotence of the strong bimonoid.

28.4.2010, 15:15 Uhr, Johannisgasse 26, 4-42
Jiamou Liu (University of Auckland und Universität Leipzig):
The Isomorphism Problem for ω-Automatic Trees

We study ω-automatic trees of finite height. These trees can be coded by ω-words in such a way that their domains and edge relations are recognized by Büchi automata. Such a tree is injectively ω-automatic if each node is represented by a unique ω-word. We present several results on the isomorphism problem for (injectively) ω-automatic trees of finite height: (i) The isomorphism problem for (injectively) ω-automatic trees of height 1 (resp. 2) is decidable (resp. Π₁⁰-complete). (ii) The isomorphism problem for injectively ω-automatic trees of height 3 is Π₁¹-hard. (iii) The isomorphism problem for (injectively) ω-automatic trees of finite height is at least as hard as second-order arithmetic and does therefore not belong to the analytical hierarchy. Moreover, assuming the continuum hypothesis, we can show that the isomorphism problem for (injectively) ω-automatic trees of finite height is interreducible with second-order arithmetic. All proofs are elementary and do not rely on theorems from set theory.

21.4.2010, 15:15 Uhr, Johannisgasse 26, 4-42
Thomas Weidner (Universität Leipzig):
On the size of injective tree automatic representations and the complexity of their computation

It has been shown that every tree automatic structure admits an injective tree automatic representation, but no good size or time bounds are known. We construct, given an arbitrary tree automatic representation as input, an injective one in single exponential time. Furthermore we show an exponential lower bound for the size of injective tree automatic representations.

Wintersemester 2009/10

18.1.2010, 14:00 Uhr, Johannisgasse 26, 4-42
Heiko Vogler (TU Dresden):
Multioperator Expressions - A Weighted MSO-logic for Trees Using Operations
(joint work with Zoltán Fülöp and Torsten Stüber)

A multioperator monoid A is a commutative monoid with additional operations on its carrier set. We define a type of weighted MSO-logic formulas over A, called multioperator expressions (M-expressions) over A. Such an M-expression is evaluated over trees and A, resulting in a tree series, i.e., a mapping from the set of trees to A. Our main result is that if A is absorptive, then the class of tree series definable by M-expressions over A coincides with the class of tree series recognizable by weighted tree automata over A. A weighted tree automaton over A is a finite state tree automaton in which each transition is equipped with an operation of A. Our main result implies the known characterization of the class of tree series recognizable by weighted tree automata over semirings in terms of syntactically restricted weighted monadic second-order logic. We prove this implication by providing two purely syntactical transformations, from M-expressions into formulas of syntactically restricted weighted monadic second-order logic, and vice versa.

17.1.2010, 10:00 Uhr, Johannisgasse 26, 4-42
Branimir Šešelja (University of Novi Sad):
Weak congruence lattice representation problem

Weak congruences of an algebra A are symmetric and transitive subuniverses of A². The poset of these is an algebraic lattice under inclusion and its sublattices are all congruence lattices of subalgebras of A and (up to an isomorphism) the subalgebra lattice of A. Representation of an algebraic lattice by the weak congruence lattice of an algebra is still an open problem in universal algebra formulated 20 years ago. Its nontrivial version is to locate an element of a lattice representing the diagonal relation and then to find a corresponding algebra. There are solutions for some special cases, e.g., the diagonal being in the center of the lattice. Many sufficient conditions have also been obtained. The aim of the talk is to present the history of the topic and some recent new results.

Andreja Tepavčević (University of Novi Sad):
Rectangular islands

A rectangular m x n board consisting of square cells is given, with a positive integer (height) associated to each cell. A rectangular island is a rectangle in the board such that the height of its cells are greater than the heights of all neighboring cells. Results concerning horizontal cuts of the height function and the connections of the obtained properties with the rectangular island systems determined by the given height function will be presented. Some combinatorial results as well as connections with fuzzy sets theory and formal concept analysis will also been given. Most of the results are obtained in cooperation with E. Horvath.

25.1.2010, 11:15 Uhr, Johannisgasse 26, 4-42
Markus Lohrey (Universität Leipzig):
Rational subsets and submonoids in groups with more than one end

In this talk I will present several results on submonoids and rational subsets of finitely generated groups that were obtained in joint work with Benjamin Steinberg. Clearly, every finitely generated submonoid of a group G is a rational subset of G. Hence, if membership in rational subsets of G is decidable, then also membership in finitely generated submonoids is decidable. In the talk, I will prove the reverse implication of this trivial implication for a large class of groups, More precisely: If G is a group with more than one end (in the sense of Hopf, 1942) and membership in finitely generated submonoids of G is decidable, then also membership in rational subsets of G is decidable. By famous results of Hopf and Stallings, the structure of groups with more than one end is well-understood.

13.1.2010, 11:15 Uhr, Johannisgasse 26, 4-42
Dietrich Kuske (Labri, Bordeaux):
Is Ramsey's theorem omega-automatic?

We study the existence of infinite cliques in omega-automatic (hyper-)graphs. It turns out that the situation is much nicer than in general uncountable graphs, but not as nice as for automatic graphs.

More specifically, we show that every uncountable omega-automatic graph contains an uncountable co-context-free clique or anticlique, but not necessarily a context-free (let alone regular) clique or anticlique. We also show that uncountable omega-automatic ternary hypergraphs need not have uncountable cliques or anticliques at all.

16.12.2009, 11:15 Uhr, Johannisgasse 26, 4-42
Roy Mennicke (Universität Leipzig):
Re-pair für Bäume

In diesem Vortrag möchte ich einen kurzen Überblick über die Inhalte meiner Diplomarbeit geben. Ich stelle einen neuen grammatik-basierten Algorithmus, genannt "Re-pair for Trees", zur Komprimierung von geordneten Bäumen über einem Rangalphabet vor. Es handelt sich dabei um eine Generalisierung des von N. Jesper Larsson im Jahr 1999 veröffentlichten Re-pair-Algorithmus. Letzterer ist ein Wörterbuch-basiertes Komprimierungsverfahren für Zeichenketten. Im Rahmen meiner Diplomarbeit habe ich einen Prototyp des Re-pair for Trees-Algorithmus, der die Baumstruktur von XML-Dokumenten komprimiert, implementiert. Dieser ermöglicht es mir Vergleiche mit anderen Grammatik-basierten Komprimierungsalgorithmen anzustellen. Die Ergebnisse zeigen, dass der Re-pair for Trees-Algorithmus seine Wettbewerber in den Punkten Komprimierungsrate, Laufzeit und Speicherverbrauch zum Teil weit hinter sich lässt. In der Praxis ist es für den Vergleich verschiedener Grammatik-basierter Komprimierungsalgorithmen nicht nur interessant, welche Komprimierungsraten bezüglich der Anzahl der Kanten der generierten Grammatik erreicht werden. Ganz wesentlich ist auch, inwieweit sich die entsprechenden Grammatiken durch eine anschließende Succintkodierung platzsparsam repräsentieren lassen. Daher stelle ich eine effiziente Binärkodierung für den von Re-pair for Trees verwendeten Typ von Baumgrammatiken vor.

9.12.2009, 11:15 Uhr, Johannisgasse 26, 4-42
Manfred Droste (Universität Leipzig):
Verbandsgewichtete Automaten und Logiken

Wir untersuchen gewichtete Automaten, rationale Ausdrücke und mehrwertige MSO-Logik mit Gewichten in beliebigen Verbänden mit 0 und 1. Wir zeigen, dass diese Formalismen für endliche und unendliche Wörter dieselbe Ausdrucksstärke haben. Dies verallgemeinert die klassischen Resultate von Kleene und Büchi auf beliebige Verbände ohne Distributivitätsvoraussetzungen, wie sie in der Theorie der Semiring-gewichteten Automaten nötig sind.

Gemeinsame Arbeit mit Heiko Vogler (TU Dresden).

4.11.2009, 11:15 Uhr, Johannisgasse 26, 4-42
Jiamou Liu (University of Auckland und Universität Leipzig):
The isomorphism problem on classes of automatic structures

A structure is automatic if its elements are coded in such a way that its domain and relations are recognizable by finite automata. The isomorphism problem on a class K of automatic structures calls for an algorithm that decides, for any given two automatic structures A,B in K, whether A is isomorphic to B. In this talk we present our new results (joint work with Dietrich Kuske and Markus Lohrey) on the isomorphism problem for some typical classes of automatic structures. In particular, we prove the following:

1. The isomorphism problem for automatic equivalence structures is undecidable (in fact Π₁⁰-complete)
2. The isomorphism problem for automatic trees of height h is Π⁰_2h-3-complete (h>1).
3. The isomorphism problem for automatic linear orders is not arithmetic (hard for every level of the arithmetic hierarchy).

28.10.2009, 11:15 Uhr, Johannisgasse 26, 4-42
Karin Quaas (Universität Leipzig):
On the supports of recognizable timed series

Recently, the model of weighted timed automata has gained interest within the real-time community. In a previous work, we built a bridge to the theory of weighted automata and introduced a general model of weighted timed automata defined over a semiring and a family of cost functions. In this model, a weighted timed automaton recognizes a timed series, i.e., a function mapping to each timed word a weight taken from the semiring. Continuing in this spirit, the aim of this paper is to investigate the support and cut languages of recognizable timed series. We present results that lead to the decidability of weighted versions of classical decidability problems as e.g. the emptiness problem. Our results may also be used to check whether weighted timed systems satisfy specifications restricting the consumption of a resource.

Sommersemester 2009

25.9.2009, 14:00 Uhr, Johannisgasse 26, 4-42
Alexander Lauser (Universität Stuttgart):
Über Quantorenalternierungen in der Logik erster Stufe mit zwei Variablen über Wörtern

Es werden verschiedene Charakterisierungen einer Hierarchie endlicher Monoide unterhalb der Varietät DA vorgestellt. Diese steht in enger Verbindung mit der Quantoren-Alternierungshierarchie in $FO^2[<]$. Exemplarisch werden wir die Äquivalenz einer algebraischen Beschreibung und einer Charakterisierung durch Gleichungen zeigen.

30.7.2009, 15:00 Uhr, Johannisgasse 26, 4-42
Claudia Nuccio (Politecnico di Milano):
Word equations on trace monoids and on inverse semigroups

In the first part of the talk are presented some results of NP-completeness for the alphabetical satisfiability problem for trace equations, i.e. the satisfiability problem for word equations on trace monoids in which it is assigned a single letter to each unknown. In the second part are given some results of decidability for multilinear word equations on amalgams of finite inverse semigroups, i.e. word equations such that each unknown occurring in them is the label of a unique edge in the Schützenberger automaton either of the left side or of the right side of the equation.

11.6.2009, 9:15 Uhr, Johannisgasse 26, 4-42
H. Herre (IMISE und IfI, Universität Leipzig):
Ontological and Logical Aspects of Mereology and Set theory

Mereology is the theory of parthood relations. These relations pertain to part to whole, and part-to-part within a whole. This area of research is today some of the core topics of ontology and conceptual modelling in computer science and artificial intelligence. In computer science and artificial intelligence the term ontology became popular since the beginning of the 1990. The mereological theory set forth in this lecture is presented as a logical theory which is formalized in first-order logic. These theories are included in the General Formal Ontology (GFO) which is a top level ontology being developed by the research group Onto-Med at the Institute for Medical Informatics (IMISE), University of Leipzig. We give an overview about the ontology of mereological systems based on the part-of relation ≤ and present results on the elementary classification of these systems. A complete and general description of the notion of whole and part which works for every situation seems to be impossible. Hence, we propose a logical framework which allows to formally capture the main aspects of parts and wholes. Furthermore, basic relations between mereology and set theory are discussed. We explore the claim expounded by David Lewis that set theory can be reduced to mereology and a small fragment of set theory pertaining to singletons. At this place the difference between the notion of set and the notion of category is crucial.

4.6.2009, 9:15 Uhr, Johannisgasse 26, 4-42
B. Steinberg (Carleton University, Ottawa & Mercator-Gastprofessor in Leipzig):
The finite Rees quotients of E-unitary inverse semigroups do not form a recursive class

Independently, Fountain and Lawson defined an inverse semigroup to be strongly 0-E-unitary if it is a Rees quotient of an E-unitary inverse semigroup by an ideal. In 2000 I showed that this problem is undecidable. The key point is that a finite inverse automaton embeds in a Cayley graph of a group if and only if its transition monoid is strongly 0-E-unitary. The problem of embeddability of a finite inverse automaton into a Cayley graph of a group is easily verified to be equivalent to the uniform word problem for groups and hence undecidable. I also consider the analogous question when we restrict to Rees quotients of E-unitary inverse semigroups with maximal group image restricted to some pseudovariety of groups.

28.5.2009, 9:15 Uhr, Johannisgasse 26, 4-42
K. Quaas:
Weighted Timed MSO Logics

We aim to generalize Büchi's fundamental theorem on the coincidence of recognizable and MSO-definable languages to a weighted timed setting. For this, we investigate subclasses of weighted timed automata and show how we can extend existing timed MSO logics with weights. Here, we focus on the class of weighted event-recording automata and define a weighted extension of the full logic MSO_er introduced by D'Souza. We show that every weighted event-recording automaton can effectively be transformed into a corresponding sentence of our logic and vice versa. The methods presented in the paper can be adopted to weighted versions of timed automata and Wilke's logic of relative distance. The results indicate the robustness of weighted timed automata models and may be used for specification purposes.

14.5.2009, 9:15 Uhr, Johannisgasse 26, 4-42
J. Koppitz (Universität Potsdam):
M-Solid (Positive) Varieties of Tree Languages

The history of the variety theory of tree languages begins with Eilenberg's variety theorem which gives a ono-to-one correspondence beween pseudovarieties of finite semigroups and varieties of recognizable languages. The variety theorem has been extended in different directions. Saeed Salehi characterized positive varieties of tree languages by pseudovarieties of ordered algebras. We consider the complete lattice of M-solid pseudovarieties of ordered algebras, where M is a monoid of hypersubstitutions.

7.5.2009, 9:15 Uhr, Johannisgasse 26, 4-42
B. Pibaljommee (Khonkaen University):
Fuzzy Subvarieties in Universal algebra

In this paper, we define the concept of fuzzy subvarieties of a variety V and show that the lattice of all subvarieties of V can be embedded into the lattice of all fuzzy subvarieties of V. Moreover, we consider the weights over a variety V and show that the lattice of all weights over V and the lattice of all fuzzy subvarieties of V are isomorphic.

30.4.2009, 9:15 Uhr, Johannisgasse 26, 4-42
M. Lohrey:
Evaluating succinct trees
(joint work with Sebastian Maneth und Manfred Schmidt-Schauss)

A well-known succinct representation of trees are directed acyclic graphs (DAGs), which allow to share several occurrences of the same subtree in a tree. In this talk we consider an even more succinct natural tree representation: hierarchical tree definitions (HTDs), which allow to share also several occurrences of the same pattern in a tree (a pattern is not necessarily a full subtree of a tree). Formally, a HTD can be defined as a context-free tree grammar that generates exactly a single tree. While it is quite obvious to evaluate a tree automaton on a given DAG in polynomial (even linear) time, this is less obvious for HTDs and was an open problem for several years. We present a polynomial time algorithm for this problem.

23.4.2009, 9:15 Uhr, Johannisgasse 26, 4-42
D. Kirsten:
On the recognizability of the supports of recognizable series

It is well-known that the support of a recogizable series is not always a recognizable language. However, for large classes of semirings (positive, locally finite, or commutative and quasi-positive semirings), it is known that the support of a recogizable series is always recognizable.

In the talk, we present another class of semirings with this property: the zero-sum free, commutative semirings. We also discuss some recent preliminary ideas which might be related to a longstanding problem in this theory: a characterization of the semirings for which the support of a recognizable series is always recognizable.

8.4.2009, 17:00 Uhr, Johannisgasse 26, Felix-Klein-Hörsaal
J. Rhodes (Berkeley):
The complexity of finite automata and semigroups: a survey

Computing the group complexity of finite automata and semigroups has been the major problem in the field for over 40 years. We give an historical summary of the technical algebraic and geometric/topological results so far developed toward the goal of proving group complexity decidable. These methods and variations have application to formal language theory, the algebraic analysis of Turing machines in Theoretical Computer Science and to various aspects of mathematics including profinite groups and semigroups. We also introduce geometric/topological methods into finite semigroup theory.

Wintersemester 2008/09

3.2.2009, 9:30 Uhr, Johannisgasse 26, 4-42
B. Steinberg (Carleton University, Ottawa & Mercator-Gastprofessor in Leipzig):
Decomposition theorems for semirings and Krohn-Rhodes complexity of power semigroups
(joint work with John Rhodes)

A natural question is: what can one say about the Krohn-Rhodes complexity of the power set of a semigroup in terms of the original semigroup? Using a new decomposition theorem for semirings, we are able to compute asymptotically (up to a factor of 2), the complexity of the power semigroup of the semigroup of all maps on n letters. We can compute exactly the complexity of the power semigroup of any inverse semigroup.

27.1.2009, 9:30 Uhr, Johannisgasse 26, 4-42
S. Göller: On the Computational Complexity of Verifying One-Counter Processes
(joint work with Richard Mayr and Anthony Widjaja To)

One-counter processes are pushdown systems over a singleton stack alphabet (plus a stack-bottom symbol). We study the complexity of two closely related verification problems over one-counter processes: model checking with the temporal logic EF in succinct representation, and weak bisimilarity checking against finite systems.

We show that both problems are $\P^\NP$-complete. This is achieved by establishing a close correspondence with the membership problem for a natural fragment of Presburger Arithmetic, which we show to be $\P^\NP$-complete. This fragment is also a suitable global representation for the global versions of the problems. We also show that there already exists a fixed EF formula (resp. a fixed finite system) such that model checking (resp. weak bisimulation) over one-counter processes is hard for $\P^{\NP[\log]}$. However, the complexity drops to $\P$ if the one-counter process is fixed.

20.1.2009, 9:30 Uhr, Johannisgasse 26, 4-42
N. Haubold: The compressed word problem in HNN-extensions

The word problem of a (finitely generated) group asks whether a word (given in some generators of the group) evaluates to the neutral element. We consider a succinct variant of this problem where the word is given in a compressed manner, using straight-line programs. We focus on HNN-extensions of finitely generated groups and show that in case the associated subgroups are finite, even a uniform variant of the compressed word problem is polynomial time Turing-reducible to the compressed word problem of the base group. We note that an analogous result holds for amalgamated products of finitely generated groups.

13.1.2009, 9:30 Uhr, Johannisgasse 26, 4-42
B. Steinberg (Carleton University, Ottawa & Mercator-Gastprofessor in Leipzig): The Cerny conjecture and group representations

The Cerny conjecture asserts that each synchronizing automaton on n states admits a synchronizing word of length at most (n-1)². A famous result of Pin says that the Cerny conjecture is valid for automata with a prime number of states such that some input cyclically permutes the states. The beautiful extension of this result to an arbitrary number of states is due to Dubuc.

Let us say that a Cayley graph of a group of order n is Cerny if every synchronizing automaton obtained from it by adjoining additional transitions admits a synchronizing word of length at most (n-1)². So Dubuc's result says in this language that the Cayley graph of a cyclic group with respect to a cyclic generating set is Cerny. Using group representation theory, we are able to provide several new infinite families of Cerny Cayley graphs coming from dihedral, symmetric, alternating, special linear and affine groups.

2.12.2008, 9:30 Uhr, Johannisgasse 26, 4-42
M. Kufleitner (Stuttgart): Fragments of first-order logic over infinite words
(joint work with V. Diekert)

We give topological and algebraic characterizations as well as language theoretic descriptions of the following subclasses of first-order logic for languages over infinite words: Σ₂, Δ₂, FO² ∩ Σ₂ (and by duality FO² ∩ Π₂), and FO². These descriptions extend the respective results for finite words. Our characterizations combine algebraic, topological, and language theoretic properties. In particular, we relate the above fragments to language classes of certain (unambiguous) polynomials.

25.11.2008, 9:30 Uhr, Johannisgasse 26, 4-42
L. Staiger (Halle): Topological Language Operators

Topological methods are useful in the theory of ω-languages in connection with proving hierarchy results. To this end one considers, for a finite alphabet X, the set of all infinite words (ω-words) over X as the Cantor-space (infinite product space of the discrete space X).

To study infinite words as limits of finite words it seems to be providing to include both into the same space. This was done by Boasson/Nivat and Redziejowski. Redziejowski observed that the limit considered by Boasson/Nivat is different from that one used in the theory of ω-automata.

Both concepts seem to have several drawbacks when considering topology in connection with acceptance of ω-words. The topology of Boasson/Nivat has all finite words as isolated points anf Redziejowski's topology has all sets consisting of only infinite words (ω-languages) as closed sets, thus providing no information on the difficulty of acceptance by topological means.

In this talk we start from the notion of δ-limit used in the theory of ω-automata and present topologies on the space X^* of all finite words which can be carried over to the product space X^ω. Because of the countability of X^* we cannot expect to obtain a full topological correspondence between the spaces X^* and X^ω via a limit operation. In fact, the δ-limit does not go beyond the class G_δ of the Borel hierarchy in X^ω but provides a correspondence between the lowest classes of the Borel hierarchy of the spaces X^* and X^ω.

18.11.2008, 9:30 Uhr, Johannisgasse 26, 4-42
M. Lohrey: Leaf languages and string compression

Tight connections between leafs languages (a concept from structural complexity theory) and strings compressed via straight-line programs (SLPs -- these are context-free grammars that generate exactly one string) are established. The compressed membership problem for a language L asks for a given SLP G, whether the string generated by G belongs to L. It is shown that the compressed membership problem for a language L is complete for the leaf language class defined by L via logspace machines. A more difficult variant of the compressed membership problem for L is shown to be complete for the leaf language class defined by L via polynomial time machines. As a corollary, it is shown that there exists a fixed linear visibly pushdown language for which the compressed membership problem is PSPACE-complete. This improves previous results.

12.11.2008, 15:00 Uhr, Johannisgasse 26, 4-42
Z. Ésik (Szeged & Tarragona): Axiomatizing rational power series

11.11.2008, 9:30 Uhr, Johannisgasse 26, 4-42
I. Meinecke: Construction of tree automata from regular expressions
(joint work with D. Kuske)

Since recognizable tree languages are closed under the rational operations, every regular tree expression denotes a recognizable tree language. We provide an alternative proof to this fact that results in smaller tree automata. To this aim, we transfer Antimirov's partial derivatives from regular word expressions to regular tree expressions. For an analysis of the size of the resulting automaton as well as for algorithmic improvements, we also transfer the methods of Champarnaud and Ziadi from words to trees.

Sommersemester 2008

22.7.2008, 14:15 Uhr, Johannisgasse 26, 4-42
M. Oppelt, J. Waldmann (HTWK Leipzig): Nichttermination

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.

15.7.2008, 15:45 Uhr, Johannisgasse 26, 4-42
Gadi Moran (University of Haifa, Israel): What is the Genus of this surface?

15.7.2008, 14:15 Uhr, Johannisgasse 26, 4-42
S. Maneth (National ICT Australia Ltd and University of New South Wales): The Equivalence Problem for MSO Definable Tree Translations

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.

17.6.2008, 14:15 Uhr, Johannisgasse 26, 4-42
A. Arikan (Ankara): Perfect Subgroups of McLain Groups

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.

3.6.2008, 14:15 Uhr, Johannisgasse 26, 4-42
M. Lohrey: Euler paths and ends in automatic and recursive graphs
(joint work with Dietrich Kuske)

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Σ⁰₃. This class consists of all set differences of Σ⁰₃ sets. The same problem for highly recursive graphs as well as automatic graphs is shown to be Π⁰₂-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.

27.5.2008, 14:15 Uhr, Johannisgasse 26, 4-42
S. Göller: ICPDL with fixed points and nominals

In meinem Vortrag werde ich die Logik μ-ICPDL_Nom 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 μ-ICPDL_Nom-Formeln sind Kripke-Strukturen. In meinem Vortag werde ich mich auf die Modelleigenschaft von μ-ICPDL_Nom konzentrieren. Es wird ein Art Entfaltungsoperator auf Kripke-Strukturen definiert, der μ-ICPDL_Nom-Theorien erhält. Daraus kann abgeleitet werden, dass jede erfüllbare μ-ICPDL_Nom-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 μ-ICPDL_Nom 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).

20.5.2008, 14:15 Uhr, Johannisgasse 26, 4-42
F. Drewes: Baumbasierte Generierung und Transformation mit TREEBAG

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.

6.5.2008, 14:15 Uhr, Johannisgasse 26, 4-42
K. Quaas: Minimale-Kosten-Überdeckungsproblem für gewichtete Petri-Netze

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).

29.4.2008, 14:15 Uhr, Johannisgasse 26, 4-42
I. Meinecke: Ein gewichteter μ-Kalkül auf Wörtern

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.

25.4.2008, 15:15 Uhr, Johannisgasse 26, 4-42
M. Droste: Normalteiler von unitären Automorphismengruppen

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 2^c 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 B_uAut(Ω), Appl. Categor. Structures 15 (2007), 153-162.

15.4.2008, 13:15 Uhr, Johannisgasse 26, 4-42
Chr. Mathissen: Weighted Logics for Nested Words and Algebraic Formal Power Series

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.

Wintersemester 2007/08

28.1.2008, 17:15 Uhr, Johannisgasse 26, 4-42
R. Peñaloza: Weighted Looping Automata

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.

22.1.2008, 11:00 Uhr, Johannisgasse 26, 4-42
D. Kirsten: Entscheidbarkeitsfragen für polynomiell mehrdeutige min-+-Automaten

14.1.2008, 17:15 Uhr, Johannisgasse 26, 4-42
D. Kuske: Compatibility of Shelah and Stupp's and of Muchnik's iteration with fragments of mondaic second order logic

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.

7.1.2008, 17:15 Uhr, Johannisgasse 26, 4-42
J. Waldmann (HTWK Leipzig): Weighted Tree Automata for Termination of Term Rewriting

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.

18.12.2007, 15:15 Uhr, Johannisgasse 26, 4-42
D. Kuske: Automatische Graphen

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.

03.12.2007, 17:15 Uhr, Johannisgasse 26, 4-42
M. Lohrey: Efficient computation in groups via compression

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)

26.11.2007, 17:15 Uhr, Johannisgasse 26, 4-42
I. Meinecke: Propositionale Dynamische Logik (PDL) für Nachrichten-Systeme

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.

12.11.2007, 17:15 Uhr, Johannisgasse 26, 4-42
M. Droste: Chu-Spaces

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:

• monic morphisms (= embeddings) of Chu spaces
• the existence of colimits of monics
• finite objects
• bifinite objects (= colimits of finite objects)
• homogeneous bifinite Chu spaces.

Reference: M. Droste and G.-Q. Zhang: Bifinite Chu spaces, in: 2nd Conf. on Algebra and Coalgebra in Computer Science (CALCO), Lecture Notes in Comp. Science vol. 4624, pp. 179-193, Springer, 2007.

6.11.2007, 15:15 Uhr, Johannisgasse 26, 4-42
G. Ulbrich: The Bergman property for full groups of measure preserving and ergodic transformations

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.

23.10.2007, 15:15 Uhr, Johannisgasse 26, 4-42
S. Göller: PDL with Intersection and Converse is 2EXP-complete

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.