We consider the parameterized verification problem for distributed algorithms where the goal is to develop techniques to prove the correctness of a given algorithm regardless of the number of participating processes. Motivated by an asynchronous binary consensus algorithm [Aspnes, 2002], we consider round-based distributed algorithms communicating with shared memory. A particular challenge in these systems is that 1) the number of processes is unbounded, and, more importantly, 2) there is a fresh set of registers at each round. A verification algorithm thus needs to manage both sources of infinity. In this setting, we prove that the safety verification problem, which consists in deciding whether all possible executions avoid a given error state, is PSPACE-complete. For negative instances of the safety verification problem, we also provide exponential lower and upper bounds on the minimal number of processes needed for an error execution and on the minimal round on which the error state can be covered.

Quantum query model has been one of the main tools in quantum computing for understanding the complexity of problems: both in terms of designing efficient algorithms, and giving lower bounds on the complexity of the problem. In case of lower bounds, the main benefit of query model is the fact that concrete mathematical techniques exist to understand the query complexity. Our main aim in this talk is to look at this computational model and see why this model has gained so much attention in the quantum computing world.

After looking at the background and definitions for the query model, we will look at reasons why quantum query complexity is an important area of study. Not just that it is one of the simplest settings to study the complexity of functions, it naturally arises in many other areas like property testing and communication complexity.

Finally, as mentioned before, there exist many mathematical tools to study quantum query complexity. We will talk about the two main lower bound methods: adversary and polynomial. It will allow us to give a very short proof that Grover search is optimal. For the case of symmetric functions, we will see that simple arguments allow us to characterize not just the query complexity but even its lower bound techniques.

Buhrman, Cleve and Wigderson (STOC'98) showed that for every Boolean function $f : \{0,1\}^n \to \{0,1\}$ and $G \in \{AND_2, XOR_2\}$, the bounded-error quantum communication complexity of the composed function ($f \circ G$) equals $O(Q(f) \log n)$, where $Q(f)$ denotes the bounded-error quantum query complexity of $f$. This is known as the BCW Simulation Theorem. This is in contrast with the classical setting, where it is easy to show that $R^{cc}(f \circ G) \leq 2R(f)$, where $R^{cc}$ and $R$ denote bounded-error communication and query complexity, respectively. We exhibited a total function for which the $\log n$ overhead in the BCW simulation is required.

We also answer several other questions related to quantum query-to-communication simulation: 1. We show that the $\log n$ overhead is not required when $f$ is symmetric (i.e., depends only on the Hamming weight of its input), generalizing a result of Aaronson and Ambainis for the Set-Disjointness function (Theory of Computing'05). 2. One may ask whether the $\log n$ overhead in the BCW Simulation Theorem can be avoided even when f is transitive, which is a weaker notion of symmetry. We show that the $\log n$ overhead is necessary for some transitive functions, even when we allow the quantum communication protocol an error probability that can be arbitrarily close to 1/2 (this corresponds to the unbounded-error model of communication). 3. We also give, among other things, a general recipe to construct functions for which the $\log n$ overhead is required in the BCW Simulation Theorem in the bounded-error communication model, even if the parties are allowed to share an arbitrary prior entangled state for free.

This talk is based on two joint works with Sourav Chakraborty, Arkadev Chattopadhyay, Peter Hoyer, Nikhil Mande, and Ronald de Wolf.

Decorated cospans are a general framework for composing open networks and mapping them to dynamical systems. We explain this framework and illustrate it with the example of stock and flow diagrams. These diagrams are widely used in epidemiology to model the dynamics of populations. Although tools already exist for building these diagrams and simulating the systems they describe, we have created a new software package called StockFlow which uses decorated cospans to overcome some limitations of existing software. Our approach cleanly separates the syntax of stock and flow diagrams from the semantics they can be assigned. We have implemented a semantics where stock and flow diagrams are mapped to ordinary differential equations, although others are possible. We illustrate this with code in StockFlow that implements a simplified version of a COVID-19 model used in Canada. This is joint work with Xiaoyan Li, Sophie Libkind, Nathaniel Osgood and Evan Patterson.

Zoom meeting registration link

YouTube live stream

Given $N\geq 1$ and $x \in [0, 1]\backslash \mathbb{Q}$, an $N$-continued fraction expansion of $x$ is defined analogously as the classical continued fraction, but with the numerators being all equal to $N$. We introduce two infinite words $\omega(x, N )$ and $\hat\omega(x, N )$ on a two letter alphabet, which are related to the $N$-continued fraction expansion of $x$ and are obtained as a limit word of a sequence of substitutions. We call them $N$-continued fraction words. When $N=1$, we are in the classical case and find a Sturmian word. We show that these words are $C$-balanced for some explicit values of $C$, and we compute the factor complexity function of both families of words. We relate this to the more general setting of limit words of non unimodular $S$-adic sequences.

This is joint work with Jörg Thuswaldner and Niels Langeveld.

The energy of a system of atoms is approximately a function of the position of the nuclei. This function is called the potential energy surface (PES). Knowledge of the PES is fundamental in ab-initio sciences but unfortunately, it cannot be computed in closed form. As a result, an important problem is that of exploring the PES to discover important features, such as local minima.

In this talk, I will introduce an experimental probabilistic programming language designed to facilitate the exploration of PES. In this language, the semantics of a program is a probability distribution over PES. The objective of the compiler is to generate an optimizer that combines solvers from machine learning and quantum chemistry to discover local minima of the PES. While much of this language and compiler is routine, we will see that the principle of conservation of energy brings about genuinely interesting compilation problems.

Since the introduction of Lüroth expansions by Lüroth in his paper from 1883 many results have appeared on their approximation properties. In 1990 Kalpazidou, Knopfmacher and Knopfmacher introduced alternating Lüroth expansions and studied their properties. A comparison between the two and other comparable number systems was then given by Barrionuevo, Burton, Dajani and Kraaikamp in 1996. In this talk we introduce a family of random dynamical systems that produce many Lüroth type expansions at once. Topics that we consider are periodic expansions, universal expansions, speed of convergence and approximation coefficients. This talk is based on joint work with Marta Maggioni.

Many computer systems are reactive: they execute in continuous interaction with their environment. From the perspective of functional programming, reactive systems can be modeled and programmed as stream functions. Several lines of research have exploited this point of view. Works based on Nakano’s guarded recursion use type-theoretical modalities to guarantee productivity. Works based on synchronous programming use more specialized methods but guarantee incremental processing of stream fragments. In this paper, we contribute to a recent synthesis between the two approaches by describing how a language with a family of type-theoretical modalities can be given an incremental semantics in the synchronous style. We prove that this semantics coincides with a more usual big-step semantics.

We study a generalization of the classic Online Joint Replenishment Problem (JRP) with Delays that we call the Online Weighted Cardinality JRP with Delays. The JRP is an extensively studied inventory management problem wherein requests for different item types arrive at various points in time. A request is served by ordering its corresponding item type. The cost of serving a set of requests depends on the item types ordered. Furthermore, each request incurs a delay penalty while it is left unserved. The objective is to minimise the total service and delay costs. In the Weighted Cardinality JRP, each item type has a positive weight and the cost of ordering is a non-decreasing, concave function of the total weight of the item types ordered. This problem was first considered in the offline setting by Cheung et al.~(2015) but nothing is known in the online setting. Our main result is a deterministic, constant competitive algorithm for this problem.