Asynchronous Distributed Automata: A Characterization of the Modal Mu-Fragment

TL;DR

This paper characterizes a class of asynchronous distributed automata by establishing their equivalence with a fragment of modal mu-calculus logic, revealing insights into their expressive power on finite directed graphs.

Contribution

It introduces a novel automaton model and proves its expressive equivalence with a specific logical fragment, independent of message loss.

Findings

Automata and logic are equivalent on finite directed graphs.

Expressive power is unaffected by message loss.

Automata use acyclic state diagrams with self-loops.

Abstract

We establish the equivalence between a class of asynchronous distributed automata and a small fragment of least fixpoint logic, when restricted to finite directed graphs. More specifically, the logic we consider is (a variant of) the fragment of the modal $\mu$-calculus that allows least fixpoints but forbids greatest fixpoints. The corresponding automaton model uses a network of identical finite-state machines that communicate in an asynchronous manner and whose state diagram must be acyclic except for self-loops. Exploiting the connection with logic, we also prove that the expressive power of those machines is independent of whether or not messages can be lost.