VSL 2014: VIENNA SUMMER OF LOGIC 2014
LCC ON SATURDAY, JULY 12TH, 2014
Days:
next day
all days

View: session overviewtalk overviewside by side with other conferences

08:45-10:15 Session 13A: LCC Opening and Invited Talk (Moser)
Location: FH, Zeichensaal 3
08:45
LCC'14 Opening Remarks
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.

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

09:45
Non-uniform Polytime Computation in the Infinitary Affine Lambda-calculus
SPEAKER: Damiano Mazza

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.

10:15-10:45Coffee Break
10:45-12:45 Session 16B: Contributed Talks
Location: FH, Zeichensaal 3
10:45
Towards recursion schemata for the probablistic class PP

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

11:15
Closing a Gap in the Complexity of Refinement Modal Logic

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 Bit-Vector Logic

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.

12:15
First-Order Logic of Order and Metric has the Three-Variable Property

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.

13:00-14:30Lunch Break
14:30-16:00 Session 18B: Invited Talk (Buss) and Contributed Talks
Location: FH, Zeichensaal 3
14:30
Search problems, proof complexity, and second-order bounded arithmetic
SPEAKER: Sam Buss

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.

15:30
Infinite AC0 Circuits for Parity

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$.

16:00-16:30Coffee Break
16:30-18:00 Session 20B: Contributed Talks
Location: FH, Zeichensaal 3
16:30
Descriptive Complexity and CSP

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.

17:00
Capturing Bisimulation-Invariant Complexity Classes with Higher-Order Modal Fixpoint Logic
SPEAKER: Etienne Lozes

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.

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