Fabian Reiter

fabian.reiter [at] gmail.com

I am a postdoctoral researcher in theoretical computer science at LSV, one of the computer science laboratories of the University of Paris-Saclay.

Academic path

Research interests

I am interested in logic and formal models of distributed computing. One of my major goals is to contribute to the recently initiated development of a descriptive complexity theory for distributed computing.

What does this mean?

Descriptive complexity basically compares the expressive powers of certain classes of algorithms, or abstract machines, with those of certain classes of logical formulas. The Holy Grail, so to speak, is to establish equivalences of the form: “Algorithm class A has exactly the same power as formula class Φ.” Probably the most famous result in this area is Fagin’s theorem from 1974, which roughly states that a graph property can be recognized by a nondeterministic Turing machine in polynomial time if and only if it can be defined by a formula of existential second-order logic. The theorem thereby provides a logical – and thus machine-independent – characterization of the complexity class NPTIME.

In general, the classical picture of descriptive complexity looks as follows:

Descriptive complexity

In my research, I aim for an extension of descriptive complexity for the classes of algorithms considered in distributed computing. This means that I seek to establish equivalences of the form: “Distributed algorithm class A has the same power as formula class Φ.”

This corresponds to the following picture:

Descriptive distributed complexity

Publications

All my publications are listed on dblp and are freely available on arXiv.

PhD thesis

My thesis, entitled “Distributed Automata and Logic”, is available here, on arXiv, and on HAL.

Abstract

Distributed automata are finite-state machines that operate on finite directed graphs. Acting as synchronous distributed algorithms, they use their input graph as a network in which identical processors communicate for a possibly infinite number of synchronous rounds. For the local variant of those automata, where the number of rounds is bounded by a constant, Hella et al. (2012, 2015) have established a logical characterization in terms of basic modal logic. In this thesis, we provide similar logical characterizations for two more expressive classes of distributed automata.

The first class extends local automata with a global acceptance condition and the ability to alternate between nondeterministic and parallel computations. We show that it is equivalent to monadic second-order logic on graphs. By restricting transitions to be nondeterministic or deterministic, we also obtain two strictly weaker variants for which the emptiness problem is decidable.

Our second class transfers the standard notion of asynchronous algorithm to the setting of nonlocal distributed automata. The resulting machines are shown to be equivalent to a small fragment of least fixpoint logic, and more specifically, to a restricted variant of the modal μ-calculus that allows least fixpoints but forbids greatest fixpoints. Exploiting the connection with logic, we additionally prove that the expressive power of those asynchronous automata is independent of whether or not messages can be lost.

We then investigate the decidability of the emptiness problem for several classes of nonlocal automata. We show that the problem is undecidable in general, by simulating a Turing machine with a distributed automaton that exchanges the roles of space and time. On the other hand, the problem is found to be decidable in logspace for a class of forgetful automata, where the nodes see the messages received from their neighbors but cannot remember their own state.

As a minor contribution, we also give new proofs of the strictness of several set quantifier alternation hierarchies that are based on modal logic.

Talk slides