View: session overviewtalk overviewside by side with other conferences
08:45  LCC'14 Opening Remarks SPEAKER: Arnold Beckmann 
08:50  Weighted Automata Theory for Complexity Analysis of Rewrite Systems SPEAKER: Georg Moser ABSTRACT. Matrix interpretations can be used to bound the derivational and runtime complexity of term rewrite systems. In particular, triangular matrix interpretations over the natural numbers are known to induce polynomial upper bounds on the complexity of (compatible) rewrite systems. Recently a couple of improvements were proposed, based on the theory of weighted automata and linear algebra. In this talk we focus on the application of weighted automata theory on the runtime complexity analysis of rewrite systems and clarify the connection to joint spectral radius theory. 
09:45  Nonuniform Polytime Computation in the Infinitary Affine Lambdacalculus SPEAKER: Damiano Mazza ABSTRACT. We give an implicit, functional characterization of the class of nonuniform polynomial time languages, based on an infinitary affine lambdacalculus and on previously defined boundedcomplexity subsystems of linear (or affine) logic. The fact that the characterization is implicit means that the complexity is guaranteed by structural properties of programs rather than explicit resource bounds. As a corollary, we obtain a proof of the (already known) Pcompleteness of the normalization problem for the affine lambdacalculus which mimics in an interesting way Ladner's Pcompleteness proof of CIRCUIT VALUE (essentially, the argument giving the CookLevin theorem). This suggests that the relationship between affine and usual lambdacalculus is deeply similar to that between Boolean circuits and Turing machines, opening some interesting perspectives, which we discuss. 
10:45  Towards recursion schemata for the probablistic class PP SPEAKER: Isabel Oitavem ABSTRACT. We propose a recursiontheoretic characterization of the probabilistic class PP, using recursion schemata with pointers. 
11:15  Closing a Gap in the Complexity of Refinement Modal Logic SPEAKER: Antonis Achilleos ABSTRACT. Refinement Modal Logic (RML), which was recently introduced by Bozzelli et al., is an extension of classical modal logic which allows one to reason about a changing model. In this paper we study computational complexity questions related to this logic, settling a number of open problems. Specifically, we study the complexity of satisfiability for the existential fragment of RML, a problem posed by Bozzelli, van Ditmarsch and Pinchinat. Our main result is a tight PSPACE upper bound for this problem, which we achieve by introducing a new tableau system. As a direct consequence, we obtain a tight characterization of the complexity of the existential fragment of RML satisfiability. 
11:45  On the Complexity of Symbolic Verification and Decision Problems in BitVector Logic SPEAKER: Gergely Kovásznai ABSTRACT. We study the complexity of decision problems encoded in bitvector logic. This class of problems includes wordlevel model checking, i.e., the reachability problem for transition systems encoded by bitvector formulas. Our main result is a generic theorem which determines the complexity of a bitvector encoded problem from the complexity of the problem in explicit encoding. In particular, NLcompleteness of graph reachability directly implies PSPACEcompleteness and EXPSPACEcompleteness for wordlevel model checking with unary and binary arity encoding, respectively. In general, problems complete for a complexity class C are shown to be complete for an exponentially harder complexity class than C when represented by bitvector formulas with unary encoded scalars, and further complete for a double exponentially harder complexity class than C with binary encoded scalars.We also show that multilogarithmic succinct encodings of the scalars result in completeness for multiexponentially harder complexity classes. Technically, our results are based on concepts from descriptive complexity theory and related techniques for OBDDs and Boolean encodings. 
12:15  FirstOrder Logic of Order and Metric has the ThreeVariable Property SPEAKER: Timos Antonopoulos ABSTRACT. Realtime specifications refer both to ordertheoretic and metric temporal properties. A natural framework for such specifications is monadic firstorder logic over the ordered real line with unary +1 function. Our main result is that this structure has the 3variable propertyevery monadic firstorder formula with at most 3 free variables is equivalent to one that uses 3 variables in total. As a corollary we obtain also the 3variable property for certain unary arithmetic functions in place of +1. As a negative example we exhibit a bijection on the reals such that the resulting structure does not have the kvariable property for any k. 
14:30  Search problems, proof complexity, and secondorder bounded arithmetic SPEAKER: Sam Buss ABSTRACT. This talk will discuss NP search problems, in particular based on the local improvement principles, in secondorder bounded arithmetic. The bounded arithmetic theory U12 captures exactly the polynomial space computable functions and predicates. It can formalize Savitch's theorem on nondeterministic space, and universal theorems in U12 translate to quasipolynomial size Frege proofs. The theory V12 plays a similar role for exponential time computable functions and predicates, and quasipolynomial size extended Frege proofs. The local improvement principles, first introduced by Kolodziejczyk, Nguyen, and Thapen, are a class of total NP search problems. The talk discusses sharpened results for characterizing the power of various local improvement principles, giving completeness results for a broader range of search problems. Most of the new results reported in this talk are joint with A. Beckmann.

15:30  Infinite AC0 Circuits for Parity SPEAKER: Benjamin Rossman ABSTRACT. For arbitrary $d,k \in \N$, we consider a firstorder theory $T$ of ``$\AC^0$ circuits of depth $d$ and size $n^k$ which compute a parity function'' where $n$ is a possibly infinite number of boolean variables. The theorem $\PARITY \notin \AC^0$ is directly equivalent to the statement that $T$ does not possess arbitrarily large finite models for all $d,k$. A slighter stronger theoremwhich follows from derandomization results of Agrawal \cite{agrawal2001towards}shows that $T$ has no pseudofinite model which includes a $\BIT$ predicate. However, unlike the theories of $\AC^0$ studied in proof complexity (which are typically formulated within Peano Arithmetic), models of $T$ are not necessary pseudofinite. In fact, the main purpose of this paper is to address the question: does $T$ have {\em any} infinite model? A negative answer would be very interesting, as $\PARITY \notin \AC^0$ would follow directly via the Compactness Theorem without recourse to finite combinatorics. Unfortunately, our main result shows this initial hope was too optimistic: we construct an infinite model of $T$ for some $d,k$ (unpublished joint work with Saharon Shelah). This counterexample leads us to consider a stronger theory, $T^<$, which augments $T$ by a linear order and axioms expressing that every definable set has a minimal element. We also consider a stricter notion of {\em definable parity function} along the lines of Ajtai \cite{ajtai1995existence}. This theory $T^<$ appears to defeat counterexamples based on symmetry. We leave it as an intriguing open question whether or not $T^<$ has any infinite model. Here again a negative answer would yield a noncombinatorial proof of $\PARITY \notin \AC^0$. 
16:30  Descriptive Complexity and CSP SPEAKER: Szymon Toruńczyk ABSTRACT. We give a common generalization of two theorems from Descriptive Complexity: 1) the ImmermanVardi theorem, which says that over linearly ordered structures, the logic LFP+C captures PTime and 2) the CaiFürerImmerman theorem, which says that over all finite structures, the logic LFP+C does not capture PTime. Our generalization relies on a connection with Constraint Satisfaction Problems and recent results from CSP theory. The results presented in this abstract are extracted from a paper [KLOT14] accepted to LICS’14. 
17:00  Capturing BisimulationInvariant Complexity Classes with HigherOrder Modal Fixpoint Logic SPEAKER: Etienne Lozes ABSTRACT. Polyadic HigherOrder Fixpoint Logic (PHFL) is a modal fixpoint logic obtained as the merger of HigherOrder Fixpoint Logic (HFL) and the Polyadic $\mu$Calculus. Polyadicity enables formulas to make assertions about tuples of states rather than states only. Like HFL, PHFL has the ability to formalise properties using higherorder functions. We consider PHFL in the setting of descriptive complexity theory: its fragment using no functions of higherorder is exactly the Polyadic $\mu$Calculus, and it is known from Otto's Theorem that it captures the bisimulationinvariant fragment of PTIME. We extend this and give capturing results for the bisimulationinvariant fragments of EXPTIME, PSPACE, and NLOGSPACE. 
17:30  Small Dynamic Descriptive Complexity Classes SPEAKER: Thomas Zeume ABSTRACT. In this talk I will give an overview over results recently obtained for small complexity classes in the dynamic descriptive complexity framework of Patnaik and Immerman. Those results are joint work with Thomas Schwentick and include a hierarchy of dynamic fragments as well as new lower bounds for the quantifierfree fragment. 