Wednesday, 9 September 2015
Show all abstracts Proceedings Close all abstracts
9:00  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 "metaanalysis" of programs in C, we can learn more about the limitations of the programs being analyzed. This essay is mostly selfcontained; 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 fixedpoint 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 SchmidtSchauss, Ashish Tiwari 
TwoRestricted One Context Unification is in Polynomial Time
Show abstract One Context Unification (1CU) extends firstorder 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 moregeneral classes of 1CU problem. Our algorithm can be seen as an extension of the usual rules of firstorder unification and can be used to solve related problems in polynomial time, such as firstorder 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, JeanPierre Jouannaud, Mizuhito Ogawa 
Confluence of layered rewrite systems
Show abstract We investigate a new, Turingcomplete 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 nonterminating, nonleftlinear, or nonright linear. Using a novel unification technique, cyclic unification, we show that rank nonincreasing layered systems are confluent provided their cyclic critical pairs have cyclicjoinable 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 secondorder 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 resourceautomatic structures. 

14:30  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 blowup incurred by turning Psi into the modal formula is shown to be necessary: there are modal formulas that can be expressed subexponentially 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 
Infinite and Biinfinite 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:
Through these results we demonstrate similarities and differences between logical properties of infinite and biinfinite words. 

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