Our group's interests in both research and teaching are in various areas within the theory of computation, among them logic, complexity theory, algorithms, and automata theory, and especially the numerous connections between these areas.
Computer Science 7 is part of the Computer Science Department within the Faculty of Mathematics, Computer Science and Natural Sciences. The chair is currently in a transition phase and will be jointly led by Prof. Grohe and Prof. Thomas for the next few years. There is a close collaboration with the Mathematical Foundations of Computer Science group.
work by Martin Grohe, Pascal Schweitzer
The question whether there is logic for polynomial time is open for more than 30 years and it remains the most important challenge
in the field of descriptive complexity theory. In my talk I summarise what is known about this question today, and I report
on very recent work which shows that rank logic, a powerful logic that was proposed by Dawar, Grohe, Holm and Laubner as a
possible solution, fails to express all polynomial-time properties (at least, in its original definition).
Room 9U09, Erweiterungsbau 3
In verification and synthesis, properties or models of interest are often quantitative, and many quantitative aspects involve
counting. For example, one might be interested in the amount of memory required by a system, how many simultaneous requests
a system has to process along a run, or how many infixes belonging to some regular language a word contains. In this talk,
we present two quantitative counting logics and two models of games with counter. We first study Qmu[#MSO], a counting logic
based on the quantitative mu-calculus. This logic is designed specifically for transition systems where the states are labeled
with finite relational structures. Counting is introduced to Qmu with the help of counting terms of monadic second-order logic,
which are evaluated on the relational structures the states are labeled with. We prove that the model-checking problem for
Qmu[#MSO] on a generalization of pushdown systems is reducible to solving finite counter parity games. We then present the
model of counter parity games, which are quantitative games in which a finite set of counters is updated along the edges.
Payoffs of finite plays are obtained via the counters, while payoffs of infinite plays are determined via a parity condition.
We show that finite counter parity games are effectively solvable, using games with imperfect recall to solve the unboundedness
problem for the value. Thus, it follows that the above model-checking problem for Qmu[#MSO] is decidable. In the last part
of the talk, we discuss a quantitative counting extension of monadic second-order logic called qcMSO and a model of games
with counters where payoffs are obtained via a mean-payoff objective on a special counter.