Tight Polynomial Bounds for Loop Programs in Polynomial Space

We consider the following problem: given a program, find tight asymptotic bounds on the values of some variables at the end of the computation (or at any given program point) in terms of its input values. We focus on the case of polynomially-bounded variables, and on a weak programming language for which we have recently shown that tight bounds for polynomially-bounded variables are computable. These bounds are sets of multivariate polynomials. While their computability has been settled, the complexity of this program-analysis problem remained open. In this paper, we show the problem to be PSPACE-complete. The main contribution is a new, space-efficient analysis algorithm. This algorithm is obtained in a few steps. First, we develop an algorithm for univariate bounds, a sub-problem which is already PSPACE-hard. Then, a decision procedure for multivariate bounds is achieved by reducing this problem to the univariate case; this reduction is orthogonal to the solution of the univariate problem and uses observations on the geometry of a set of vectors that represent multivariate bounds. Finally, we transform the univariate-bound algorithm to produce multivariate bounds.

A Block-Sparse Tensor Train Format for Sample-Efficient High-Dimensional Polynomial Regression

Low-rank tensors are an established framework for the parametrization of multivariate polynomials. We propose to extend this framework by including the concept of block-sparsity to efficiently parametrize homogeneous, multivariate polynomials with low-rank tensors. This provides a representation of general multivariate polynomials as a sum of homogeneous, multivariate polynomials, represented by block-sparse, low-rank tensors. We show that this sum can be concisely represented by a single block-sparse, low-rank tensor.We further prove cases, where low-rank tensors are particularly well suited by showing that for banded symmetric tensors of homogeneous polynomials the block sizes in the block-sparse multivariate polynomial space can be bounded independent of the number of variables.We showcase this format by applying it to high-dimensional least squares regression problems where it demonstrates improved computational resource utilization and sample efficiency.

Strategic Reasoning in Automated Mechanism Design

Mechanism Design aims at defining mechanisms that satisfy a predefined set of properties, and Auction Mechanisms are of foremost importance. Core properties of mechanisms, such as strategy-proofness or budget-balance, involve: (i) complex strategic concepts such as Nash equilibria, (ii) quantitative aspects such as utilities, and often (iii) imperfect information,with agents’ private valuations. We demonstrate that Strategy Logic provides a formal framework fit to model mechanisms, express such properties, and verify them. To do so, we consider a quantitative and epistemic variant of Strategy Logic. We first show how to express the implementation of social choice functions. Second, we show how fundamental mechanism properties can be expressed as logical formulas,and thus evaluated by model checking. Finally, we prove that model checking for this particular variant of Strategy Logic can be done in polynomial space.

Designed quadrature to approximate integrals in maximum simulated likelihood estimation

Maximum simulated likelihood estimation of mixed multinomial logit models requires evaluation of a multidimensional integral. Quasi-Monte Carlo (QMC) methods such as Halton sequences and modified Latin hypercube sampling are workhorse methods for integral approximation. Earlier studies explored the potential of sparse grid quadrature (SGQ), but SGQ suffers from negative weights. As an alternative to QMC and SGQ, we looked into the recently developed designed quadrature (DQ) method. DQ requires fewer nodes to get the same level of accuracy as of QMC and SGQ, is as easy to implement, ensures positivity of weights, and can be created on any general polynomial space. We benchmarked DQ against QMC in a Monte Carlo and an empirical study. DQ outperformed QMC in all considered scenarios, is practice-ready and has potential to become the workhorse method for integral approximation.

Approximate Counting of k -Paths: Simpler, Deterministic, and in Polynomial Space

Recently, Brand et al. [STOC 2018] gave a randomized mathcal O(4 k m ε -2 -time exponential-space algorithm to approximately compute the number of paths on k vertices in a graph G up to a multiplicative error of 1 ± ε based on exterior algebra. Prior to our work, this has been the state-of-the-art. In this article, we revisit the algorithm by Alon and Gutner [IWPEC 2009, TALG 2010], and obtain the following results: • We present a deterministic 4 k + O (√ k (log k +log 2 ε -1 )) m -time polynomial-space algorithm. This matches the running time of the best known deterministic polynomial-space algorithm for deciding whether a given graph G has a path on k vertices. • Additionally, we present a randomized 4 k +mathcal O(log k (log k +logε -1 )) m -time polynomial-space algorithm. Our algorithm is simple—we only make elementary use of the probabilistic method. Here, n and m are the number of vertices and the number of edges, respectively. Additionally, our approach extends to approximate counting of other patterns of small size (such as q -dimensional p -matchings).

The Effects of Adding Reachability Predicates in Quantifier-Free Separation Logic

The list segment predicate ls used in separation logic for verifying programs with pointers is well suited to express properties on singly-linked lists. We study the effects of adding ls to the full quantifier-free separation logic with the separating conjunction and implication, which is motivated by the recent design of new fragments in which all these ingredients are used indifferently and verification tools start to handle the magic wand connective. This is a very natural extension that has not been studied so far. We show that the restriction without the separating implication can be solved in polynomial space by using an appropriate abstraction for memory states, whereas the full extension is shown undecidable by reduction from first-order separation logic. Many variants of the logic and fragments are also investigated from the computational point of view when ls is added, providing numerous results about adding reachability predicates to quantifier-free separation logic.

Efficient loop-check for multimodal KD45n logic

We introduce sequent calculus for multi-modal logic KD45n which uses efficient loop-check. Efficiency of the used loop-check is obtained by using marked modal operator squarei which is used as an alternative to sequent with histories ([2,3]).We use inference rules with or branches to make all rules invertible or semi-invertible. We showthe maximum height of the constructed derivation tree. Also polynomial space complexity is proved.

New Algorithms for Mixed Dominating Set

A mixed dominating set is a collection of vertices and edges that dominates all vertices and edges of a graph. We study the complexity of exact and parameterized algorithms for \textsc{Mixed Dominating Set}, resolving some open questions. In particular, we settle the problem's complexity parameterized by treewidth and pathwidth by giving an algorithm running in time $O^*(5^{tw})$ (improving the current best $O^*(6^{tw})$), as well as a lower bound showing that our algorithm cannot be improved under the Strong Exponential Time Hypothesis (SETH), even if parameterized by pathwidth (improving a lower bound of $O^*((2 - \varepsilon)^{pw})$). Furthermore, by using a simple but so far overlooked observation on the structure of minimal solutions, we obtain branching algorithms which improve both the best known FPT algorithm for this problem, from $O^*(4.172^k)$ to $O^*(3.510^k)$, and the best known exponential-time exact algorithm, from $O^*(2^n)$ and exponential space, to $O^*(1.912^n)$ and polynomial space. Comment: This paper has been accepted to IPEC 2020

L 1 -Multiscale Galerkin’s Scheme with Multilevel Augmentation Algorithm for Solving Time Fractional Burgers’ Equation

In this paper, we consider the initial boundary value problem of the time fractional Burgers equation. A fully discrete scheme is proposed for the time fractional nonlinear Burgers equation with time discretized by L 1 -type formula and space discretized by the multiscale Galerkin method. The optimal convergence orders reach O τ 2 − α + h r in the L 2 norm and O τ 2 − α + h r − 1 in the H 1 norm, respectively, in which τ is the time step size, h is the space step size, and r is the order of piecewise polynomial space. Then, a fast multilevel augmentation method (MAM) is developed for solving the nonlinear algebraic equations resulting from the fully discrete scheme at each time step. We show that the MAM preserves the optimal convergence orders, and the computational cost is greatly reduced. Numerical experiments are presented to verify the theoretical analysis, and comparisons between MAM and Newton’s method show the efficiency of our algorithm.