Abstract
In a recent article, Lauri Hella and coauthors identify a canonical connection between modal logic and deterministic distributed constanttime 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 codefinable by a modal theory. A class C is codefinable 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 \mucalculus 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.
BibTeX  Entry
@InProceedings{kuusisto:LIPIcs:2013:4213,
author = {Antti Kuusisto},
title = {{Modal Logic and Distributed Message Passing Automata}},
booktitle = {Computer Science Logic 2013 (CSL 2013)},
pages = {452468},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783939897606},
ISSN = {18688969},
year = {2013},
volume = {23},
editor = {Simona Ronchi Della Rocca},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2013/4213},
URN = {urn:nbn:de:0030drops42132},
doi = {10.4230/LIPIcs.CSL.2013.452},
annote = {Keywords: Modal logic, message passing automata, descriptive characterizations, distributed computing}
}
Keywords: 

Modal logic, message passing automata, descriptive characterizations, distributed computing 
Seminar: 

Computer Science Logic 2013 (CSL 2013) 
Issue Date: 

2013 
Date of publication: 

27.08.2013 