Modal Logic and Distributed Message Passing Automata (Preliminary Draft)

Abstract

In a recent article, Lauri Hella and co-authors identify a canonical connection between modal logic and deterministic distributed constant-time algorithms. The paper reports a variety of highly natural logical characterizations of classes of distributed message passing automata that run in constant time. However, the article leaves open the question of identifying related logical characterizations when the constant running time limitation is lifted. We obtain such a characterization for a class of finite message passing automata in terms of a recursive bisimulation invariant logic we call modal substitution calculus (MSC). We also give a logical characterization of the related class A of infinite message passing automata by showing that classes of labelled directed graphs recognizable by automata in A are exactly the classes co-definable by a modal theory. A class C is co-definable by a modal theory if the complement of C is definable by a possibly infinite set of modal formulae. We also briefly discuss expressivity and decidability issues concerning MSC. We establish that MSC contains the mu-1 fragment of the modal mu-calculus in the finite. We also observe that MSC is not contained in MSO, and that the SAT and FINSAT problems for the single-variable fragment of MSC are complete for PSPACE. This article is a preliminary draft of an upcoming paper. A polished and corrected version will appear later on.