VErification, Logic, and CRyptOgraphy

Title to be announced

A. R. Balasubramanian Max Planck Institute for Software Systems

Dicey Games: Shared Sources of Randomness in Distributed Systems

Léonard Brice Institute of Science and Technology Austria

Systems that interact synchronously with an unpredictable environment are usually captured by zero-sum concurrent games. In such games, randomised strategies are in general more powerful than deterministic ones. Such systems, however, do not capture faithfully decentralised systems that cannot resort to a common private source of randomness. In this talk, I will introduce dicey games, a model for games played by teams, where the structure of randomness sources accessible to each player is explicitly specified.

Intersecting Dense Automata: Constructions, Complexity and Certificates

Neha Rino University of Warwick

Given $k$ nondeterministic finite automata (NFA), finding an NFA that recognises the intersection of their languages is a basic problem in automata theory. We observe that the classical Cartesian product construction is non-optimal in the worst case, that is, if the automata have many transitions. For a fixed alphabet, the Cartesian product of two NFA may have $\Theta(m^2)$ transitions if these NFA have at most $n$ states and $m$ transitions each.

In this talk, we describe alternative constructions with $O(mn)$ transitions; or $O(mn^{k-1})$ for the intersection of $k$ NFA (for fixed $k \geq 2$ and alphabet $\Sigma$). This gives a faster algorithm for deciding NFA intersection emptiness, that is, deciding whether $k$ given NFA accept a word in common.

We also show that this new algorithm is optimal, unless there exists a breakthrough combinatorial algorithm for detecting cliques in undirected graphs.

Joint work with Dmitry Chistikov.

Decoupled Planning for Multiple Omega-Regular Objectives

Suman Sadhukhan TU Clausthal

Imagine you need to generate a path on a graph that satisfies several $\omega$-regular objectives at once. The standard approach is to build one monolithic plan for their conjunction. But what if one of the objectives is replaced? Do we have to redesign the plan from scratch? In this talk, I will explore a more modular alternative: give each objective to its own agent, let each agent pick a local policy, and have a scheduler, who knows nothing about the graph or the objectives, decide on the fly whose policy to follow at each step.

The question I’ll focus on is simple to state: assuming the conjunction of all objectives is realizable, when does this kind of composition actually satisfy all of them?

I’ll show that scheduling alone isn’t enough, even with randomization, and that agents need some coordination, and a synchronization protocol for safety. I’ll then introduce conventions, simple rules agreed on before the graph or objectives are known, that guarantee all objectives are met, and discuss how much information each class of objectives requires, from Büchi to parity.

Joint work with Guy Avni, Kaushik Mallik, Thejaswini K S, and Thomas A. Henzinger.

Clustering in Varying Metrics

Ankita Sarkar Ashoka University

We consider a variant of center-based $k$-clustering in which the underlying metric space varies; this is modeled as $T$ different distance functions $d_1$, $d_2$, $\ldots$, $d_T$ on the same point set $C$. The goal is to pick a $k$-sized subset $S \subseteq C$ such that, with $S$ as the cluster centers, some “aggregate” cost across the $T$ metric spaces is minimized. Such an aggregate cost can be, for example, the sum of the $T$ many $k$-center costs that $S$ incurs in each metric. This problem models, for example, the task of locating new hospitals in an area prone to monsoon-based road closures. More broadly, this aggregate variant models center-based clustering tasks where distances are seasonal but the choice of centers is inflexible. In this talk, we understand the inapproximability and special-case approximability of a few different aggregate $k$-clustering problems, and encounter related open problems.

Bounds on Polynomial Approximations for the Discrete Logarithm

Ashutosh Shankar TIFR, Mumbai

Abstract to be announced.

Category Theory and Topology for Logic and Verification

Brandon Shapiro Florida Gulf Coast University

Homotopy Type Theory, broadly construed, uses syntax rules from computer science as a system for verifiable constructions and proofs about “types” which can model a wide range of algebraic and spatial structures from mathematics. This talk will survey these ideas and their wide-ranging applications for a computer science audience.

Title to be announced

A. R. Sricharan University of Macau

New Approaches to Liquid Democracy

Michelle Yeo Aarhus University and NTU

Liquid democracy is a transitive vote delegation mechanism over voting graphs. A central question in the sphere of delegated voting is when does liquid democracy outperform direct voting. In this talk, I will examine this question from two perspectives. In the first, I will look at liquid democracy in a setting with a ground truth voting outcome. Previously, Kahng et al. showed that it is impossible for liquid democracy to always outperform direct voting in general voting graphs in this setting. Specifically, there are graph topologies that result in every voter delegating their voters to a “dictator”, which can have a potential negative impact on the final voting result. In this talk, I will show positive results for liquid democracy for specific graph topologies. A common feature of these graph topologies is that they preserve a certain amount of variance in the delegation process, which has implications on fairness in voting graphs. In the second perspective, I will examine liquid democracy when there is no ground truth voting outcome, and instead two opposing factions. I will show an interesting result that vote delegation enables the weaker faction to win the election with higher probability compared to direct voting, implying that delegation can be fairer than direct voting for the weaker faction.