Fabian Reiter

fabian.reiter [at] univ-eiffel.fr

I am an assistant professor (maître de conférences) in theoretical computer science at Gustave Eiffel University (formerly University of Paris-Est Marne-la-Vallée).

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

Academic work

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

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

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.