Research Seminar Logic and Automata
Talks in Winter Term 2010/2011
- Finite Model Theory with Operators from Linear Algebra
Wednesday, 19 January 2011, 11:30, Seminar Room of Informatik 7 (Room 4116)
Wied Pakusa RWTH Aachen University
Whether there is a logic that captures PTIME is one of the major open questions in the field of descriptive complexity theory. For some time, the extension of least fixed point logic by counting quantifiers, FP+C, appeared to be very promising in this concern, but in their famous work Cai, Fürer and Immerman were able to rule out FP+C as a possible candidate. Nevertheless, it has been shown that FP+C captures PTIME on many interesting domains of structures. While the first classes that were established to separate FP+C from PTIME appeared to be rather artificial, recent results of Dawar et. al revealed that they all reduce to the very natural problem of deciding solvability of linear equation systems over finite fields. This situation motivates to analyze the descriptive complexity of problems from linear algebra and of extensions of logics by operators from linear algebra.
In our work we review and broaden the achieved results and make some new contributions to this active area of research. In particular we generalize investigations from finite fields to finite commutative rings. We demonstrate that many problems from linear algebra that are known to be definable in FP+C over finite fields remain definable over finite rings. We further enrich this class by providing a definition of the minimal polynomial in FP+C. Considering logical operators for solvability of linear equation systems, matrix similarity, matrix equivalence and matrix rank, we obtain various proper extensions of FP+C. Restricted to finite fields, we are able to arrange these extensions in a hierarchy. We also make some progress on relating them in the general case. Finally, we show that for the case of solvability operators, one can restrict to quotient rings Z/nZ without loosing expressive power.
- Definability on omega-Automatic Structures
Monday, 14 February 2011, 13:00, Seminar Room of Informatik 7 (Room 4116)
Faried abu Zaid RWTH Aachen University
Automatic structures are structures that can be represented over a regular domain such that all its relations and functions can also be recognized by finite automata. Automatic structures can be considered over different types of underlying automata. In particular one can consider automata over finite words or trees and over infinite words or trees yielding [omega][tree]-automatic structures. Since important problems such as first order model checking and query evaluation can be done effectively on this presentations, they give a robust framework for algorithmic model theory. Today one of the main tasks is to explore the boundaries of this classes. For the case of finite word automata some techniques were developed to show that a structure is not automatic but for the other classes not too much is known.
In our work we focus on omega-automatic structures. We present three approaches for showing that a structure is not omega-automatic. First we transfer the concept of growth rates from automatic structures to omega-automatic structures and explain why this notion will most probably fail as a tool for proofing non-automaticity. Next we discuss the use sub-presentations. We show that every presentation of a uncountable linear order contains an injective presentation of the lexicographic order on the set of all infinite 0-1-sequences. With this result it is possible to show that there are no uncountable automatic ordinals. At last we identify a property of automatic relations and words that are equal from some fixed position onwards and apply it to show that the are no injective presentations of pairing functions.
- ATL with strategy contexts
Tuesday, 15 February 2011, 15:00, Seminar Room of Informatik 7 (Room 4116)
Nicolas Markey ENS Cachan
We study the alternating-time temporal logics ATL and ATL* extended with strategy contexts: these make agents commit to their strategies during the evaluation of formulas, contrary to plain ATL and ATL* where strategy quantifiers reset previously selected strategies.
We prove that the resulting logics ATLsc and ATL*sc are very powerful, and particularly well-suited for expressing properties of non-zero-sum games. We also propose a model-checking algorithm for these extensions, based on alternating tree automata. The algorithm runs in k-EXPSPACE (where k is the number of strategy quantifiers).
- Dynamic Definability
Thursday, 17 February 2011, 11:30, Seminar Room of Informatik 7 (Room 4116)
Sebastian Siebertz RWTH Aachen University
Dynamic definability theory studies the resources required to maintain knowledge about a fixed property of a structure that is object to an ongoing sequence of minor changes. An important application of dynamic complexity is the incremental maintenance of views in relational databases. Two equivalent frameworks for modeling dynamic systems were introduced by Patnaik and Immerman (called Dyn-FO) and Dong et al. (called first-order incremental evaluation systems, FOIES).
It was shown that many properties which cannot be queried by first-order logic (or equivalently, relational calculus) can indeed be maintained in the dynamic setting, e.g. reachability in acyclic graphs, reachability in undirected graphs and bipartiteness. Both settings assume that the dynamic process starts with an empty structure. Weber and Schwentick generalized the setting such that the dynamic process can start with an arbitrary ordered structure.
We adapt the descriptive setting of Weber and Schwentick, i.e. we consider finite relational structures where auxiliary data consists of relations over the domain of the input structure. Initialization of the auxiliary structure and all updates are handled by logical interpretations. However, we do not assume that the given structures are ordered. We show that many upper bounds for concrete problems also hold in this case. Our search for incremental evaluation systems on unordered structures actually yielded systems where the auxiliary data is independent of the update history. In the literature such systems are called memoryless or deterministic. In particular, we provide a deterministic FOIES for reachability in symmetric graphs and it follows via dynamic reduction that many other problems have deterministic FOIES as well. We show how to modify the dynamic algorithm of Etessami for tree isomorphism to obtain a deterministic incremental evaluation system with first-oder + counting updates.
On the other hand we show that in our unordered setting we can maintain neither equal cardinality nor tree isomorphism with first-order updates. On ordered structures or equivalently when the dynamic process starts with an empty structure such lower bounds are extremely hard to obtain.
- Logics with unary and guarded negations.
Monday, 21 February 2011, 16:00, Seminar Room of Informatik 7 (Room 4116)
Luc Segoufin ENS Cachan
Modal logic and its extension with fixpoints, the mu-calculus, are "robustly" decidable. The reason is that they have the tree model property (if a formula has a model, it has one that is a tree), they have the finite model property (if there is a model there is a finite one), they are included into MSO and hence can be translated into tree automata. These properties immediately imply decidability.
Is it possible to extends modal logics while maintaining those nice properties?
This led to the introduction of guarded logics limiting quantifications to tuples of the model. One can then see that they are fragments of guarded logics and guarded logics enjoy good properties: tree-like model property (if there is a model there is one of bounded tree-width), finite model property and interpretation into MSO (recognizing the tree decompositions of the models). These nice properties immediately imply decidability.
In this talk we will first introduce another orthogonal extension of modal logics while retaining all the nice properties stated above. We will see that restricting the quantification to existential quantification and negations to formulas having at most one free variable yield natural extension of modal logic and the mu-calculus having finite model property, tree-like model property, and decidability.
Finally we will see that limiting negations to guarded formulas extends at the same time the guarded fragment and the unary negation fragment while retaining all the nice properties. Altogether this work provides fairly expressive and natural decidable fragments of FO and FixPoint logics.
- Banach-Mazur Games with Simple Winning Strategies
Wednesday, 16 March 2011, 11:00, Seminar Room of Informatik 7 (Room 4116)
Simon Lessenich RWTH Aachen University
Banach-Mazur games on graphs correspond to the natural notion of path games, i.e. two-player games on graphs where the moves are finite paths instead of just single edges. Such Banach-Mazur games on graphs are a special case of their topological variant, hence general results on determinacy for topological Banach-Mazur games also hold in the graph setting. However, general winning strategies are complex objects. Thus, concepts of simple strategies are needed which are strong enough in the sense that many important classes of Banach-Mazur games are determined via these simple strategies.
In our work we focus on Muller winning conditions, mainly over a countably infinite set of colors, and a generalization of these winning conditions, where the objective is to see certain words of colors infinitely often while avoiding others. For games with winning conditions of either type we study different concepts of simple winning strategies. As positional strategies do not suffice for Muller winning conditions over a countably infinite set of colors, and since finite memory strategies can be reduced to positional ones, we investigate strategies that have access to restricted kinds of infinite memory. We discuss two variants, namely counting strategies and strategies using FAR-memory, and observe that many classes of the previously mentioned winning conditions guarantee determinacy via such strategies.
As boundedness of the lengths of moves may be needed or desired for applications of Banach-Mazur games on graphs, we also look at two notions of bounded strategies and study the effects of restricting players to these.
- Solving Muller Games via Safety Games
Tuesday, 22 March 2011, 10:00, Seminar Room of Informatik 7 (Room 4116)
Wladimir Fridman, Daniel Neider, Roman Rabinovich, Martin Zimmermann RWTH Aachen University
We consider the problem of determining the winner in a Muller game. The classical reduction constructs a parity game of size n!, which preserves the winner and allows to derive a finite-state winning strategy. Here, we use new results on finite-duration Muller games to reduce the decision problem "Does Player 0 win a given Muller game?" to the same problem for safety games of size (n!)^3. Hence, we have to solve a (potentially) simpler type of game on an arena which is only polynomially larger than the parity game. Furthermore, we present a proof-of-concept implementation of our algorithm. This is ongoing research.
- Memory Reduction via Delayed Simulation
Tuesday, 22 March 2011, 10:30, Seminar Room of Informatik 7 (Room 4116)
Marcus Gelderie RWTH Aachen University
We address a central (and classical) issue in the theory of infinite games: the reduction of the memory size that is needed to implement winning strategies in regular infinite games (i.e., controllers that ensure correct behavior against actions of the environment, when the specification is a regular omega-language). We propose an approach which attacks this problem before the construction of a strategy, by first reducing the game graph that is obtained from the specification. For the cases of specifications represented by "request-response"-requirements and general "fairness" conditions, we show that an exponential gain in the size of memory is possible.