Coalgebraic Reasoning with Global Assumptions in Arithmetic Modal Logics

We establish a generic upper bound ExpTime for reasoning with global assumptions (also known as TBoxes) in coalgebraic modal logics. Unlike earlier results of this kind, our bound does not require a tractable set of tableau rules for the instance logics, so that the result applies to wider classes of logics. Examples are Presburger modal logic, which extends graded modal logic with linear inequalities over numbers of successors, and probabilistic modal logic with polynomial inequalities over probabilities. We establish the theoretical upper bound using a type elimination algorithm. We also provide a global caching algorithm that potentially avoids building the entire exponential-sized space of candidate states, and thus offers a basis for practical reasoning. This algorithm still involves frequent fixpoint computations; we show how these can be handled efficiently in a concrete algorithm modelled on Liu and Smolka’s linear-time fixpoint algorithm. Finally, we show that the upper complexity bound is preserved under adding nominals to the logic, i.e., in coalgebraic hybrid logic.

Variable Smoothing for Weakly Convex Composite Functions

We study minimization of a structured objective function, being the sum of a smooth function and a composition of a weakly convex function with a linear operator. Applications include image reconstruction problems with regularizers that introduce less bias than the standard convex regularizers. We develop a variable smoothing algorithm, based on the Moreau envelope with a decreasing sequence of smoothing parameters, and prove a complexity of $${\mathcal {O}}(\epsilon ^{-3})$$ O ( ϵ - 3 ) to achieve an $$\epsilon $$ ϵ -approximate solution. This bound interpolates between the $${\mathcal {O}}(\epsilon ^{-2})$$ O ( ϵ - 2 ) bound for the smooth case and the $${\mathcal {O}}(\epsilon ^{-4})$$ O ( ϵ - 4 ) bound for the subgradient method. Our complexity bound is in line with other works that deal with structured nonsmoothness of weakly convex functions.

All Classical Adversary Methods Are Equivalent for Total Functions

We show that all known classical adversary lower bounds on randomized query complexity are equivalent for total functions and are equal to the fractional block sensitivity fbs( f ). That includes the Kolmogorov complexity bound of Laplante and Magniez and the earlier relational adversary bound of Aaronson. This equivalence also implies that for total functions, the relational adversary is equivalent to a simpler lower bound, which we call rank-1 relational adversary. For partial functions, we show unbounded separations between fbs( f ) and other adversary bounds, as well as between the adversary bounds themselves. We also show that, for partial functions, fractional block sensitivity cannot give lower bounds larger than √ n ⋅ bs( f ), where n is the number of variables and bs( f ) is the block sensitivity. Then, we exhibit a partial function f that matches this upper bound, fbs( f ) = Ω (√ n ⋅ bs( f )).

Tableau-based Decision Procedure for Non-Fregean Logic of Sentential Identity

Sentential Calculus with Identity ($$\mathsf {SCI}$$ SCI ) is an extension of classical propositional logic, featuring a new connective of identity between formulas. In $$\mathsf {SCI}$$ SCI two formulas are said to be identical if they share the same denotation. In the semantics of the logic, truth values are distinguished from denotations, hence the identity connective is strictly stronger than classical equivalence. In this paper we present a sound, complete, and terminating algorithm deciding the satisfiability of $$\mathsf {SCI}$$ SCI -formulas, based on labelled tableaux. To the best of our knowledge, it is the first implemented decision procedure for $$\mathsf {SCI}$$ SCI which runs in NP, i.e., is complexity-optimal. The obtained complexity bound is a result of dividing derivation rules in the algorithm into two sets: decomposition and equality rules, whose interplay yields derivation trees with branches of polynomial length with respect to the size of the investigated formula. We describe an implementation of the procedure and compare its performance with implementations of other calculi for $$\mathsf {SCI}$$ SCI (for which, however, the termination results were not established). We show possible refinements of our algorithm and discuss the possibility of extending it to other non-Fregean logics.

Types for Complexity of Parallel Computation in Pi-Calculus

Type systems as a technique to analyse or control programs have been extensively studied for functional programming languages. In particular some systems allow to extract from a typing derivation a complexity bound on the program. We explore how to extend such results to parallel complexity in the setting of the pi-calculus, considered as a communication-based model for parallel computation. Two notions of time complexity are given: the total computation time without parallelism (the work) and the computation time under maximal parallelism (the span). We define operational semantics to capture those two notions, and present two type systems from which one can extract a complexity bound on a process. The type systems are inspired both by size types and by input/output types, with additional temporal information about communications.

Empirical Q-Value Iteration

We propose a new simple and natural algorithm for learning the optimal Q-value function of a discounted-cost Markov decision process (MDP) when the transition kernels are unknown. Unlike the classical learning algorithms for MDPs, such as Q-learning and actor-critic algorithms, this algorithm does not depend on a stochastic approximation-based method. We show that our algorithm, which we call the empirical Q-value iteration algorithm, converges to the optimal Q-value function. We also give a rate of convergence or a nonasymptotic sample complexity bound and show that an asynchronous (or online) version of the algorithm will also work. Preliminary experimental results suggest a faster rate of convergence to a ballpark estimate for our algorithm compared with stochastic approximation-based algorithms.

COMPLEXITY OF THE INFINITARY LAMBEK CALCULUS WITH KLEENE STAR

We consider the Lambek calculus, or noncommutative multiplicative intuitionistic linear logic, extended with iteration, or Kleene star, axiomatised by means of an $\omega $ -rule, and prove that the derivability problem in this calculus is $\Pi _1^0$ -hard. This solves a problem left open by Buszkowski (2007), who obtained the same complexity bound for infinitary action logic, which additionally includes additive conjunction and disjunction. As a by-product, we prove that any context-free language without the empty word can be generated by a Lambek grammar with unique type assignment, without Lambek’s nonemptiness restriction imposed (cf. Safiullin, 2007).

On the complexity of an augmented Lagrangian method for nonconvex optimization

In this paper we study the worst-case complexity of an inexact augmented Lagrangian method for nonconvex constrained problems. Assuming that the penalty parameters are bounded we prove a complexity bound of $\mathcal{O}(|\log (\epsilon )|)$ outer iterations for the referred algorithm to generate an $\epsilon$-approximate KKT point for $\epsilon \in (0,1)$. When the penalty parameters are unbounded we prove an outer iteration complexity bound of $\mathcal{O}(\epsilon ^{-2/(\alpha -1)} )$, where $\alpha>1$ controls the rate of increase of the penalty parameters. For linearly constrained problems these bounds yield to evaluation complexity bounds of $\mathcal{O}(|\log (\epsilon )|^{2}\epsilon ^{-2})$ and $\mathcal{O}(\epsilon ^{- (\frac{2(2+\alpha )}{\alpha -1}+2 )})$, respectively, when appropriate first-order methods ($p=1$) are used to approximately solve the unconstrained subproblems at each iteration. In the case of problems having only linear equality constraints the latter bounds are improved to $\mathcal{O}(|\log (\epsilon )|^{2}\epsilon ^{-(p+1)/p})$ and $\mathcal{O}(\epsilon ^{-(\frac{4}{\alpha -1}+\frac{p+1}{p})})$, respectively, when appropriate $p$-order methods ($p\geq 2$) are used as inner solvers.

Model-Based Synthesis of Incremental and Correct Estimators for Discrete Event Systems

State tracking, i.e. estimating the state over time, is always an important problem in autonomous dynamic systems. Run-time requirements advocate for incremental estimation and memory limitations lead us to consider an estimation strategy that retains only one state out of the set of candidate estimates at each time step. This avoids the ambiguity of a high number of candidate estimates and allows the decision system to be fed with a clear input. However, this strategy may lead to dead-ends in the continuation of the execution. In this paper, we show that single-state trackability can be expressed in terms of the simulation relation between automata. This allows us to provide a complexity bound and a way to build estimators endowed with this property and, moreover, customizable along some correctness criteria. Our implementation relies on the Sat Modulo Theory solver MonoSAT and experiments show that our encoding scales up and applies to real world scenarios.

An Improved FPT Algorithm for Independent Feedback Vertex Set

We study the Independent Feedback Vertex Set problem — a variant of the classic Feedback Vertex Set problem where, given a graph G and an integer k, the problem is to decide whether there exists a vertex set $S\subseteq V(G)$ S ⊆ V ( G ) such that G ∖ S is a forest and S is an independent set of size at most k. We present an $\mathcal {O}^{\ast }((1+\varphi ^{2})^{k})$ O ∗ ( ( 1 + φ 2 ) k ) -time FPT algorithm for this problem, where φ < 1.619 is the golden ratio, improving the previous fastest $\mathcal {O}^{\ast }(4.1481^{k})$ O ∗ ( 4.148 1 k ) -time algorithm given by Agrawal et al. (2016). The exponential factor in our time complexity bound matches the fastest deterministic FPT algorithm for the classic Feedback Vertex Set problem. On the technical side, the main novelty is a refined measure of an input instance in a branching process, that allows for a simpler and more concise description and analysis of the algorithm.