Friday, 08.05.2015
12:30

13:30
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 polynomialtime properties (at least, in its original definition).
Wednesday, 13.05.2015
14:00

15:00
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 mucalculus. 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 secondorder logic,
which are evaluated on the relational structures the states are labeled with. We prove that the modelchecking 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 modelchecking problem for Qmu[#MSO] is decidable. In the last part
of the talk, we discuss a quantitative counting extension of monadic secondorder logic called qcMSO and a model of games
with counters where payoffs are obtained via a meanpayoff objective on a special counter.