Computer Science Logic 2015
Berlin, 7-10 September 2015
Technische Universität Berlin

Wednesday, 9 September 2015

9:00 Ryan Williams
Ryan Williams
Thinking Algorithmically About Impossibility
Show abstract

Complexity lower bounds like P != NP assert impossibility results for all possible programs of some restricted form. As there are presently enormous gaps in our lower bound knowledge, a central question on the minds of today's complexity theorists is how will we find better ways to reason about all efficient programs?

I argue that some progress can be made by (very deliberately) thinking algorithmically about lower bounds. Slightly more precisely, to prove a lower bound against some class C of programs, we can start by treating C as a set of inputs to another (larger) process, which is intended to perform some basic analysis of programs in C. By carefully studying the algorithmic "meta-analysis" of programs in C, we can learn more about the limitations of the programs being analyzed.

This essay is mostly self-contained; scant knowledge is assumed of the reader.

10:00 Erich Grädel, Wied Pakusa Rank logic is dead, long live rank logic!
Show abstract

Motivated by the search for a logic for polynomial time, we study rank logic (FPR) which extends fixed-point logic with counting (FPC) by operators that determine the rank of matrices over finite fields. While FPR can express most of the known queries that separate FPC from PTIME, nearly nothing was known about the limitations of its expressive power.

In our first main result we show that the extensions of FPC by rank operators over different prime fields are incomparable. This solves an open question posed by Dawar and Holm and also implies that rank logic, in its original definition with a distinct rank operator for every field, fails to capture polynomial time. In particular we show that the variant of rank logic FPR* with an operator that uniformly expresses the matrix rank over finite fields is more expressive than FPR.

One important step in our proof is to consider solvability logic FPS which is the analogous extension of FPC by quantifiers which express the solvability problem for linear equation systems over finite fields. Solvability logic can easily be embedded into rank logic, but it is open whether it is a strict fragment. In our second main result we give a partial answer to this question: in the absence of counting, rank operators are strictly more expressive than solvability quantifiers.

10:30 Coffee break (Room H 3005)
11:00 Adria Gascon, Manfred Schmidt-Schauss, Ashish Tiwari
Adria Gascon, Manfred Schmidt-Schauss, Ashish Tiwari
Two-Restricted One Context Unification is in Polynomial Time
Show abstract

One Context Unification (1CU) extends first-order unification by introducing a single context variable. This problem was recently shown to be in NP, but it is not known to be solvable in polynomial time. We show that the case of 1CU where the context variable occurs at most twice in the input (1CU2r) is solvable in polynomial time. Moreover, a polynomial representation of all solutions can also be computed in polynomial time. The 1CU2r problem is important as it is used as a subroutine in polynomial time algorithms for several more-general classes of 1CU problem. Our algorithm can be seen as an extension of the usual rules of first-order unification and can be used to solve related problems in polynomial time, such as first-order unification of two terms that tolerates one clash. All our results assume that the input terms are represented as Directed Acyclic Graphs.

11:30 Jiaxiang Liu, Jean-Pierre Jouannaud, Mizuhito Ogawa
Jiaxiang Liu, Jean-Pierre Jouannaud, Mizuhito Ogawa
Confluence of layered rewrite systems
Show abstract

We investigate a new, Turing-complete class of layered systems, whose linearized lefthand sides of rules can only be overlapped at the root position. Layered systems define a natural notion of rank for terms: the maximal number of redexes along a path from the root to a leaf. Overlappings are allowed in finite or infinite trees. Rules may be non-terminating, non-left-linear, or non-right- linear. Using a novel unification technique, cyclic unification, we show that rank non-increasing layered systems are confluent provided their cyclic critical pairs have cyclic-joinable decreasing diagrams.

12:00 Ackermann Award Ceremony
13:00 Lunch break
14:00 Lukasz Kaiser, Martin Lang, Simon Leßenich, Christof Löding A unified approach to boundedness properties in MSO
Show abstract

In the past years, extensions of monadic second-order logic (MSO) that can specify boundedness properties by the use of operators referring to the sizes of sets have been considered. In particular, the logics costMSO introduced by T. Colcombet and MSO+U by M. Bojanczyk were analyzed and connections to automaton models have been established to obtain decision procedures for these logics. In this work, we propose the logic quantitative counting MSO (qcMSO for short), which combines aspects from both costMSO and MSO+U. We show that both logics can be embedded into qcMSO in a natural way. Moreover, we provide a decidability proof for the theory of its weak variant (quantification only over finite sets) for the natural numbers with order and the infinite binary tree. These decidability results are obtained using a regular cost function extension of automatic structures called resource-automatic structures.

14:30 Karoliina Lehtinen, Sandra Quickert
Karoliina Lehtinen, Sandra Quickert
Constructive decidability of the first levels of the modal mu alternation hierarchy
Show abstract

We construct, for any sentence of the modal mu calculus Psi, derived sentences in the modal fragment and the fragment without least fixpoints of the modal mu calculus such that Psi is equivalent to a formula in these fragments if and only if it is equivalent to these formulas. The formula without greatest fixpoints that Psi is equivalent to if and only if it is equivalent to any formula without greatest fixpoint is obtained by duality. This yields a constructive proof of decidability of the first levels of the modal mu alternation hierarchy. The blow-up incurred by turning Psi into the modal formula is shown to be necessary: there are modal formulas that can be expressed sub-exponentially more efficiently with the use of fixpoints. For the fragments with only greatest or least fixpoints however, as long as formulas are in disjunctive form, the transformation into a formula syntactically in these fragments does not increase the size of the formula.

15:00 Dietrich Kuske, Jiamou Liu, Anastasia Moskvina
Dietrich Kuske, Jiamou Liu, Anastasia Moskvina
Infinite and Bi-infinite Words with Decidable Monadic Theories
Show abstract

We study word structures of the form $(D,<,P)$ where $D$ is either $\N$ or $\Z$, $<$ is a linear ordering on $D$ and $P\subseteq D$ is a predicate on $D$. In particular we show:

  1. The set of recursive $\omega$-words with decidable monadic second order theories is $\Sigma_3$-complete.

  2. We characterise those sets $P\subseteq\Z$ that yield bi-infinite words $(\Z,\le,P)$ with decidable monadic second order theories.

  3. We show that such "tame" predicates $P$ exist in every Turing degree.

  4. We determine, for $P\subseteq\Z$, the number of predicates $Q\subseteq\Z$ such that $(\Z,\le,P)$ and $(\Z,\le,Q)$ are indistinguishable.

Through these results we demonstrate similarities and differences between logical properties of infinite and bi-infinite words.

15:30 The busses for the excursion leave in front of the main building
16:00 Excursion to Potsdam
19:30 Conference Dinner