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.

The  talk is  based  on  joint work  with  Aart Middeldorp,  Friedrich Neurauter, Johannes Waldmann, and Harald Zankl.

ABSTRACT. We give an implicit, functional characterization of the class of non-uniform polynomial time languages, based on an infinitary affine lambda-calculus and on previously defined bounded-complexity 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) P-completeness of the normalization problem for the affine lambda-calculus which mimics in an interesting way Ladner's P-completeness proof of CIRCUIT VALUE (essentially, the argument giving the Cook-Levin theorem). This suggests that the relationship between affine and usual lambda-calculus is deeply similar to that between Boolean circuits and Turing machines, opening some interesting perspectives, which we discuss.

ABSTRACT. We propose a recursion-theoretic characterization of the probabilistic class PP, using recursion schemata with pointers.

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.

ABSTRACT. We study the complexity of decision problems encoded in bit-vector logic. This class of problems includes word-level model checking, i.e., the reachability problem for transition systems encoded by bit-vector formulas. Our main result is a generic theorem which determines the complexity of a bit-vector encoded problem from the complexity of the problem in explicit encoding. In particular, NL-completeness of graph reachability directly implies PSPACE-completeness and EXPSPACE-completeness for word-level 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 bit-vector 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 multi-logarithmic succinct encodings of the scalars result in completeness for multi-exponentially harder complexity classes. Technically, our results are based on concepts from descriptive complexity theory and related techniques for OBDDs and Boolean encodings.

ABSTRACT. Real-time specifications refer both to order-theoretic and metric temporal properties. A natural framework for such specifications is monadic first-order logic over the ordered real line with unary +1 function. Our main result is that this structure has the 3-variable property---every monadic first-order formula with at most 3 free variables is equivalent to one that uses 3 variables in total. As a corollary we obtain also the 3-variable 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 k-variable property for any k.

ABSTRACT. This talk will discuss NP search problems, in particular based on the local improvement principles, in second-order bounded arithmetic.  The bounded arithmetic theory U-1-2 captures exactly the polynomial space computable functions and predicates.  It can formalize Savitch's theorem on non-deterministic space, and universal theorems in U-1-2 translate to quasipolynomial size Frege proofs.  The theory V-1-2 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.

ABSTRACT. For arbitrary $d,k \in \N$, we consider a first-order 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 theorem---which 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 non-combinatorial proof of $\PARITY \notin \AC^0$.

ABSTRACT. We give a common generalization of two theorems from Descriptive Complexity: 1) the Immerman-Vardi theorem, which says that over linearly ordered structures, the logic LFP+C captures PTime and 2) the Cai-Fürer-Immerman 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.

ABSTRACT. Polyadic Higher-Order Fixpoint Logic (PHFL) is a modal fixpoint logic obtained as the merger of Higher-Order 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 higher-order functions. We consider PHFL in the setting of descriptive complexity theory: its fragment using no functions of higher-order is exactly the Polyadic $\mu$-Calculus, and it is known from Otto's Theorem that it captures the bisimulation-invariant fragment of PTIME. We extend this and give capturing results for the bisimulation-invariant fragments of EXPTIME, PSPACE, and NLOGSPACE.

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 quantifier-free fragment.