ABSTRACT. We consider a variant of string constraints given by membership constraints in context-free languages and subword relation between variables. The satisfiability problem for this variant turns out to be undecidable. We consider a fragment in which the subword order constraints do not impose any cyclic dependency between variables. We show that this fragment is NEXPTIME-complete. As an application of our result, we settle the complexity of control state reachability in acyclic lossy channel pushdown systems, an important distributed system model. The problem was shown to be decidable by Atig et al. in 2008. However, no elementary upper bound was known. We show that this problem is NEXPTIME-complete.

ABSTRACT. Workflow nets are a popular variant of Petri nets that allow for the algorithmic formal analysis of business processes. The central decision problems concerning workflow nets deal with soundness, where the initial and final configurations are specified. Intuitively, soundness states that from every reachable configuration one can reach the final configuration. We settle the widely open complexity of the three main variants of soundness: classical, structural and generalised soundness. The first two are EXPSPACE-complete, and, surprisingly, the latter is PSPACE-complete, thus computationally simpler.

ABSTRACT. We study the complexity of the reachability problem for Vector Addition Systems with States (VASSes) in fixed dimensions. We provide four lower bounds improving the currently known state-of-art: 1) NP-hardness for unary flat 4-VASSes (VASSes in dimension 4), 2) PSpace-hardness for unary 5-VASSes, 3) ExpSpace-hardness for binary 6-VASSes and 4) Tower-hardness for unary 8-VASSes.

ABSTRACT. Probabilistic pushdown automata (recursive state machines) are a widely known model of probabilistic computation associated with many decidable problems about termination (time) and linear-time model checking. Higher-order recursion schemes (HORS) are a prominent formalism for the analysis of higher-order computation. Recent studies showed that, for the probabilistic variant of HORS, even the basic problem of determining whether a scheme terminates almost surely is undecidable. Moreover, the undecidability already holds for order-2 schemes (order-1 schemes are known to correspond to pushdown automata). Motivated by these results, we study restricted probabilistic tree-stack automata (rPTSA), which in the nondeterministic setting are known to characterise a proper extension of context-free languages, namely, the multiple context-free languages. We show that several verification problems, such as almost-sure termination, positive almost-sure termination and omega-regular model checking are decidable for this class. At the level of higher-order recursion schemes, this corresponds to being able to verify a probabilistic version of the so-called affine-additive higher-order recursion schemes (PAHORS). PAHORS extend order-1 recursion schemes and are incomparable with order-2 schemes.

ABSTRACT. Automatic structures are infinite structures that are finitely represented by synchronized finite-state automata. We investigate Ramsey quantifiers over automatic structures, which express the existence of infinite cliques in an edge relation, and observe connections to two problems in verification: (1) reachability with (generalized) Büchi conditions in regular model checking can be seen as Ramsey quantification over transitive automatic graphs, (2) checking monadic decomposability of automatic relations can be viewed as Ramsey quantification over co-transitive automatic graphs. We provide a comprehensive complexity landscape of Ramsey quantifiers, all between NL and EXP, which yields a wealth of new results with precise complexity.

ABSTRACT. An infinite-state system is bidirected (sometimes called reversible) if for every transition, there exists another with opposite effect. We study reachability in bidirected systems in the framework of valence systems, an abstract model featuring finitely many control states and an infinite-state storage that is specified by a finite graph. Picking suitable graphs yields counters as in vector addition systems, pushdowns, integer counters, and combinations. We provide a comprehensive complexity analysis. For example, the complexity of bidirected reachability drops substantially (often to polynomial time) from that of general reachability, for almost every storage mechanism where general reachability is known to be decidable.

ABSTRACT. LREC= is an extension of first-order logic with a logarithmic recursion operator. It was introduced by Grohe et al. and shown to capture the complexity class L (log-space) over trees and interval graphs. It does not capture L in general as it is contained in FPC - fixed-point logic with counting. We show that this containment is strict. In particular, we show that the path systems problem, a classic P-complete problem which is definable in LFP - fixed-point logic - is not definable in LREC. This shows that the logarithmic recursion mechanism is provably weaker than general least fixed points.

ABSTRACT. Can the lambda-calculus be considered as a reasonable computational model? Can we use it for measuring the time and space consumption of algorithms? While the literature contains positive answers about time, much less is known about space. This paper presents a new reasonable space cost model for the lambda-calculus, given by the space used by a variant over the Krivine abstract machine, and which is the first one able to account for logarithmic space. Moreover, we study the time behavior of our machine and show how to transport the results to the call-by-value lambda-calculus.

ABSTRACT. Circular (or cyclic) proofs have received increasing attention in recent years, and have been proposed as an alternative setting for studying (co)inductive reasoning. In particular, now several type systems based on circular reasoning have been proposed. However, little is known about the complexity theoretic aspects of circular proofs, which exhibit sophisticated loop structures atypical of more common 'recursion schemes'.

This paper attempts to bridge the gap between circular proofs and implicit computational complexity (ICC). Namely we introduce a circular proof system based on Bellantoni and Cook's famous safe-normal function algebra, and we identify proof theoretical constraints, inspired by ICC, to characterise the polynomial-time and elementary computable functions. Along the way we introduce new recursion theoretic implicit characterisations of these classes that may be of interest in their own right.

ABSTRACT. We study the Radical Identity Testing problem (RIT): Given an algebraic circuit representing a multivariate polynomial $f(x_1, \dots, x_k)$ and nonnegative integers $a_1, \dots, a_k$ and $d_1, \dots, d_k$, written in binary, test whether the polynomial vanishes at the real radicals $\sqrt[d_1]{a_1}, \dots,\sqrt[d_k]{a_k}$, i.e., test whether $f(\sqrt[d_1]{a_1}, \dots, \sqrt[d_k]{a_k}) = 0$. We place the problem in coNP assuming the Generalised Riemann Hypothesis (GRH), improving on the straightforward PSPACE upper bound obtained by reduction to the existential theory of reals. Next we consider a restricted version, called 2-RIT, where the radicals are square roots of prime numbers, written in binary. It was known since the work of Chen and Kao that 2-RIT is at least as hard as the polynomial identity testing problem, however no better upper bound than PSPACE was known prior to our work. We show that 2-RIT is in coRP assuming GRH and in coNP unconditionally. Our proof relies on theorems from algebraic and analytic number theory, such as the Chebotarev density theorem and quadratic reciprocity.

ABSTRACT. We study how the complexity of modular circuits computing AND depends on the depth of the circuits and the prime factorization of the modulus they use. In particular, our construction of subexponential circuits of depth 2 for AND helps us to classify (modulo Exponential Time Hypothesis) modular circuits with respect to the complexity of their satisfiability. We also study a precise correlation between this complexity and the sizes of modular circuits realizing AND. On the other hand showing that AND can be computed by a polynomial size probabilistic modular circuit of depth 2 (with O(log n) random bits) providing a probabilistic computational model that can not be derandomized.

We apply our methods to determine (modulo ETH) the complexity of solving equations over groups of symmetries of regular polygons with an odd number of sides. These groups form a paradigm for some of the remaining cases in characterizing finite groups with respect to the complexity of their equation solving.

ABSTRACT. We extend Choiceless Polynomial Time (CPT), the currently only remaining promising candidate in the quest for a logic capturing PTime, so that this extended logic has the following property: for every class of structures for which isomorphism is definable, the logic automatically captures PTime.

For the construction of this logic we extend CPT by a witnessed symmetric choice operator. This operator allows for choices from definable orbits. But, to ensure polynomial time evaluation, automorphisms have to be provided to certify that the choice set is indeed an orbit.

We argue that, in this logic, definable isomorphism implies definable canonization. Thereby, our construction removes the non-trivial step of extending isomorphism definability results to canonization. This step was a part of proofs that show that CPT or other logics capture PTime on a particular class of structures. The step typically required substantial extra effort.

ABSTRACT. Given epsilon and a Boolean formula F, the problem of almost-uniform generation seeks to generate solutions such that every solution is generated with a probability that is within (1+epsilon)-multiplicative factor of 1/#F where #F is the number of solutions of F. The problem of almost-uniform generation was shown to be inter-reducible to that of randomized approximate counting in the seminal work of Jerrum, Valiant, and Vazirani (TCS, 1986). The proposed reduction, however, requires a linear number of calls to approximate counter, and therefore, provides an O(n log (n) log (n/epsilon)) algorithm that employs pairwise independent hash functions.

In this work, we propose a new algorithm that makes only one call to the approximate counter, and in turn, provides an O( log n * log (1/epsilon) + 1/epsilon) algorithm for an almost-uniform generation. The key ingredient of our approach is a beautiful combination of the usage of approximate counting and 3-wise independent hash functions. Since the standard tabulation-based hash family proposed by Carter and Wegman (STOC 1977) is known to be 3-wise independent, our scheme can be highly efficient in practical applications where a SAT solver is typically used in lieu of a NP oracle. We demonstrate that theoretical improvements translate to practice; in particular, we conduct a comprehensive study over 562 benchmarks and demonstrate that while JVV would time out for 544 out of 562 instances, our proposed scheme can handle all the 562 instances. To the best of our knowledge, this is the first almost-uniform generation scheme that can handle practical instances from real-world applications. We also present a nuanced analysis focusing on the both the size of SAT queries as well as the number of queries.

ABSTRACT. We introduce the novel machinery of smooth approximations, and apply it to confirm the CSP dichotomy conjecture for first-order reducts of the random tournament, and to give new short proofs of the conjecture for various homogeneous graphs including the random graph (STOC'11, ICALP'16), and for expansions of the order of the rationals (STOC'08). Apart from obtaining these dichotomy results, we show how our new proof technique allows to unify and significantly simplify the previous results from the literature. For all but the last structure, we moreover characterise for the first time those CSPs which are solvable by local consistency methods, again using the same machinery.

ABSTRACT. We prove the following completeness result about classical realizability: given any Boolean algebra with at least two elements, there exists a Krivine-style classical realizability model whose characteristic Boolean algebra is elementarily equivalent to it. This is done by controlling precisely which combinations of so-called "angelic" (or "may") and "demonic" (or "must") nondeterminism exist in the underlying model of computation.