License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2013.452
URN: urn:nbn:de:0030-drops-42132
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4213/
Go to the corresponding LIPIcs Volume Portal

Kuusisto, Antti

Modal Logic and Distributed Message Passing Automata

pdf-format:
33.pdf (0.4 MB)

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. 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.

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 =	{452--468},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Simona Ronchi Della Rocca},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4213},
  URN =		{urn:nbn:de:0030-drops-42132},
  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
Collection: Computer Science Logic 2013 (CSL 2013)
Issue Date: 2013
Date of publication: 02.09.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI