Arbeitsgemeinschaft Logik und Automaten

Vorträge im Wintersemester 2004/05


Di, 29.3.2005, 11:00 Uhr
Thomas Colcombet, IRISA Rennes


We consider the extension of the monadic second-order logic with an extra quantifier B. This logic is abbreviated by MSOB for ``monadic second-order with bounds''. The meaning of the new construction BX.Phi is that there is a bound on the size of finite sets X satisfying Phi. The dual of B is U, and UX.Phi can be interpreted as ``there are sets X satisfying Phi as big as I want''. In MSOB, those operators B and U can be combined with all the usual ones: existential and universal quantifications as well as boolean operations, complementation included. This logic is strictly more expresive than standard MSO.

In this talk we will present the logic MSOB and show that some nontrivial fragments are decidable over the structure (N,Succ).

This is joint work with M. Bojanczyk.

On Preservation in Classes of Finite Structures

Mi, 9.3.2005, 11:00 Uhr
Anuj Dawar, University of Cambridge


Connectivity and Decompositions of Directed Graphs

Do, 3.3.2005, 14:00 Uhr
Jan Obdrzalek, RWTH Aachen


Tree width is now an estabilished notion for measuring connectivity of (undirected) graphs. Graphs with low tree-width allow decomposition of the problem being solved into subproblems, decreasing the overall complexity. Many otherwise NP-complete problems are solvable in polynomial time when restricted to these graphs. Also winner in a parity game can easily be decided in polynomial time on graphs of bounded treewidth.

However, a similar measure for directed graphs is hard to come by. TJohnson, Robertson, Seymour and Thomas in 1999 introduced "directed tree width". In this talk I will argue why this measure is not adequate for many purposes (e.g. solving parity games in polynomial time) and discuss some of the ways how to define the "right" measure.

Alternatively, I'll talk about the recent paper claiming to give an algorithm solving parity games in polynomial time.

Pushdown Games

Di, 15.2.2005, 11:00 Uhr
Olivier Serre, LIAFA Paris


Two-player pushdown games provide a natural model for infinite open systems: the program is represented by the first player, Eve, and the environment is represented by the second player, Adam. In this framework, Eve has a winning strategy if and only if there exists a controller for the program that ensures that a property, described by the winning condition, is satisfied.

For these games, one can consider several winning conditions. If one is interested in verification, classical winning conditions (reachability, Buchi, parity) and more specific conditions (as the one concerning the height of the stack) are natural. In a more theoretical approach, one can consider winning conditions having arbitrary high finite Borel complexity.

In this talk, we present a large variety of decidable winning conditions for pushdown games and give intuition on how one can simulate these games by simpler ones and hence get a "general" technique to decide the winner in various pushdown games.

Decidability of MSO Theories of Deterministic Tree Structures

Mo, 24.1.2005, 13:30 Uhr
Gabriele Puppis, Università Udine


We address the verification problem for systems of monadic second-order logic interpreted over deterministic tree structures. We achieve an automaton-based solution to this problem in two steps: first, we reduce the considered problem to the problem of determining, for any Rabin tree automaton, whether it accepts a given labeled tree; then, we exploit a suitable notion of tree equivalence to reduce (a number of instances of) the latter problem to the decidable case of regular trees. We prove that such a reduction works for a large class of trees, that we call residually regular trees. Then, we show that the proposed technique can be used to decide the theories of some meaningful relational structures, including trees in the Caucal hierarchy and trees outside it.

The Controlled Linear Programming Problem

Do, 13.1.2005, 14:00 Uhr
Henrik Björklund, Uppsala University


The controlled linear programming problem (CLPP) is a combinatorial optimization problem. An instance consists of a number of linear constraints of a certain form. A controller is allowed select and discard constraints according to simple rules, with the goal of maximizing the optimal solution to the resulting linear program.

The CLPP captures and generalizes parity, mean payoff, discounted payoff, and simple stochastic games. For its most general version, the exact complexity is still unknown, but several rich subclasses can be shown to belong to NP intersection coNP. In this talk we use linear algebra to characterize the properties of such subclasses, and prove a number of new results. We also identify sufficient conditions for a class to be solvable in randomized subexponential time.

Parikh Automata with Pushdown Stack

Do, 16.12.2004, 14:00 Uhr
Wong Karianto, RWTH Aachen


Parikh automata are a new automata model introduced by Klaedtke and Ruess; the model of finite automata is combined with arithmetical constraints expressible in the framework of semi-linear sets. One of their main results is that the emptiness problem for this model is decidable, which relies on the fact that the Parikh images (that is, the images under the Parikh mapping) of regular languages are semi-linear and that the emptiness problem for semi-linear sets is decidable.

In this thesis, we investigate the possibilities of extending the idea underlying Parikh automata to pushdown automata (PDA) and level 2 pushdown automata (2PDA), which are automata augmented with stacks consisting of stacks.

For the former, we show that the emptiness problem is still decidable, as already noted by Klaedtke and Ruess in their work on Parikh automata. Moreover, we show that Parikh automata and Parikh-PDA's recognize only context-sensitive languages.

For the latter, we investigate the Parikh images of 2PDA-recognizable languages. We extend the framework of semi-linear sets to the so-called semi-polynomial sets and show that 2PDA's can generate all these sets. However, we also show that there are 2PDA-recognizable languages whose Parikh images are not semi-polynomial.

Finally, for the issue of using semi-polynomial sets as the constraint sets of Parikh automata, we investigate the emptiness problem for the intersection of a semi-linear set and a semi-polynomial set. We show two partial results: first, weakening the framework of semi-linear sets leads to decidability, and second, strengthening the framework of semi-polynomial sets leads to undecidability.

Note: If there is still time remaining, we will briefly look at the application of the idea underlying Parikh automata to infinite graphs.

Kombinatorische Auktionen (Light)

Do, 11.11.2004, 14:00 Uhr
Dietmar Berwanger, RWTH Aachen


In kombinatorischen Auktionen können Gebote für Bündel von Gütern abgegeben werden. Der Auktionator teilt die Güter daraufhin den Bietern zu und setzt dafür jeweils Preise bis zur Gebotlinie fest. Bereits pragmatische Überlegungen führen zu der Einsicht, dass sich eine erfolgreichen Auktion hauptsächlich auf das Gemeinwohl ausrichten sollte, d.h. dass die Schätzung der Bieter für das ihnen jeweils zugeteilte B¨ndel in der Summe unübertreffbar ist. Allerdings ist diese Schätzung dem Auktionator nicht unmittelbar bekannt; um darauf schließen zu können, muss die Preisberechnung gewissen Wahrhaftigkeitkriterien folgen, die sich wiederum aus der Lösung eines Optimierungsproblems ergeben.

Structural Algorithm for Parity Games

Do, 21.10.2004, 16:00 Uhr
Jan Obdrzalek, RWTH Aachen


Parity games are well known infinite games of two players, with still unknown precise complexity of solving them. In this talk I will present a new algorithm for solving parity games. Comparing to the other currently known algorithms, this one tries hard to focus on the structure of the game graph. I will present a structure called "spine" and show some of its properties. Then I will talk about computation on this structure, and show that some obvious exponential-time cases are not possible in this scenario. Some connections to the strategy improvement algorithm of Vöge and Jurdzinski will be mentioned as well.

This is joint work with Colin Stirling.

Network Ressource Allocation

Do, 14.10.2004, 14:00 Uhr
Philipp Rohde, RWTH Aachen


This talk was given during the GI-Dagstuhl-Seminar 'Game-Theoretic Analyses of the Internet' (August 30 - September 03, 2004) and is based on the work of F.P. Kelly, R. Johari, and J.N. Tsitsiklis.

We consider charging and rate control for network resources. We assume a collection of users submitting bids (willingness-to-pay per unit) for links, and a single network manager allocating the capacities. The utility for each user is measured in monetary units depending on his allocated rate. We assume smooth utility functions corresponding to an 'elastic traffic'.

We may distinguish two different frameworks: Price taking users do not anticipate the effect of their bidding on the price, whereas for price anticipating users the model becomes a game. In the first case we show the existence of a pricing scheme maximizing the aggregate utility subject to the given capacity bounds (social optimum). In fact this optimization problem can be decomposed into subsidiary problems (one for each user and one for the manager), where a Lagrange multiplier mediates. For the game between selfish users we can find a unique Nash equilibrium.

One may ask whether the anticipating behavior significantly worsen the performance. We quantify the loss of efficiency ('price of anarchy') by showing that the Nash equilibrium of the game leads to a total utility which is no worse than 3/4 the social optimum. We conclude by considering the relation between certain fairness criteria and an appropriate choice of utility functions.