VErification, Logic, and CRyptOgraphy

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.

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.

Joint work with Deeparnab Chakrabarty and Jonathan Conroy.

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.

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.

Given a network and many packet demands to route, an optimal solution can be found by solving a multicommodity flow problem when the demands are known beforehand. If the demands arrive online, the best solution would be to perform a demand-aware routing, which remembers how all previous requests were routed when routing the current request. A simple-to-implement alternative, which routes each demand independent of all others, is an oblivious routing.

Examples include maintaining a set of $\Omega(m)$ spanning trees, then randomly selecting a tree and routing along the unique tree path, or maintaining a set of $\Omega(\sqrt{m})$ resistance assignments to the edges, then randomly selecting one and routing the request as if the graph was an electrical network. For constructing a single object and not a set to sample from, the best known result is to maintain a dominating tree on the vertices, which gives $O(\log^2 n \log \log n)$ competitive ratio. We show that there is a single setting of resistances that can be imposed on the network which achieves optimal $O(\log n)$ competitive ratio for oblivious routing.

Nested counter systems (NCS) are a generalization of counter systems to higher-order counters. Here, a higher-order counter is allowed to have other (lower-order) counters as elements, instead of just a number. Such systems can be viewed as working on trees, where the height of the tree naturally corresponds to the highest order counter that the system is working with. It is known that the coverability problem for NCS, which asks if a given final tree can be covered from a given initial tree, is $F_{\epsilon_0}$-complete. Here $F_{\epsilon_0}$ is a class in the fast-growing hierarchy of complexity classes.

In this work, we consider an extension of NCS called nested reset counter systems (NRCS) that extends NCS with resets. We show that coverability for NRCS over order-$k$ counters is $F_{\Omega_k}$-complete where $\Omega_k$ is the tower of height $k$ of the $\omega$ ordinal. This gives the first natural hierarchy of complete problems for all of these classes. Furthermore, to prove our upper bounds, we also develop length function theorems for any fixed amount of applications of the multiset operation on finite sets.

As an application of our results, we improve existing upper bounds for various problems from XML processing, graph transformation systems, $\pi$-calculus, logic and parameterized verification. Furthermore, using our completeness results for $k$-NRCS, we also prove $F_{\Omega_k}$-completeness of the considered problems from the realms of parameterized verification and logic, for all $k$.

Joint work with Franzisco Schmidt.

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.

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.