Modal Logic and Distributed Message Passing Automata

Author Antti Kuusisto

Thumbnail PDF


  • Filesize: 396 kB
  • 17 pages

Document Identifiers

Author Details

Antti Kuusisto

Cite AsGet BibTex

Antti Kuusisto. Modal Logic and Distributed Message Passing Automata. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 452-468, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


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. 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 which 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 Sigma^\mu_1 fragment of the modal \mu-calculus in the finite. We also observe that the single variable fragment MSC^1 of MSC is not contained in MSO, and that the SAT and FINSAT problems of MSC^1 are complete for PSPACE.
  • Modal logic
  • message passing automata
  • descriptive characterizations
  • distributed computing


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads