The MSO theory of connectedly communicating processes

P. Madhusudan, P. S. Thiagarajan, Shaofa Yang

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We identify a network of sequential processes that communicate by synchronizing frequently on common actions. More precisely, we demand that there is a bound k such that if the process p executes k steps without hearing from process q - directly or indirectly - then it will never hear from q again. The non-interleaved branching time behavior of a system of connectedly communicating processes (CCP) is given by its event structure unfolding. We show that the monadic second order (MSO) theory of the event structure unfolding of every CCP is decidable. Using this result, we also show that an associated distributed controller synthesis problem is decidable for linear time specifications that do not discriminate between two different linearizations of the same partially ordered execution.

Original languageEnglish (US)
Title of host publicationFSTTCS 2005
Subtitle of host publicationFoundations of Software Technology and Theoretical Computer Science - 25th International Conference, Proceedings
Pages201-212
Number of pages12
DOIs
StatePublished - Dec 1 2005
Event25th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2005 - Hyderabad, India
Duration: Dec 15 2005Dec 18 2005

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3821 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other25th International Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2005
CountryIndia
CityHyderabad
Period12/15/0512/18/05

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'The MSO theory of connectedly communicating processes'. Together they form a unique fingerprint.

Cite this