Dynamic Message Sequence charts

Martin Leucker, P. Madhusudan, Supratik Mukhopadhyay

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

Abstract

We introduce a formalism to specify classes of MSCs over an unbounded number of processes. The formalism can describe many interesting behaviours of dynamically changing networks of processes. Moreover, it strictly includes the formalism of Message Sequence Graphs studied in the literature to describe MSCs over a fixed finite set of processes. Our main result is that model-checking of MSCs described in this formalism against a suitable monadic-second order logic is decidable.

Original languageEnglish (US)
Title of host publicationFST TCS 2002
Subtitle of host publicationFoundations of Software Technology and Theoretical Computer Science - 22nd Conference, Proceedings
EditorsManindra Agrawal, Anil Seth
PublisherSpringer
Pages253-264
Number of pages12
ISBN (Print)3540002251, 9783540002253
DOIs
StatePublished - 2002
Externally publishedYes
Event22nd International Conference on the Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2002 - Kanpur, India
Duration: Dec 12 2002Dec 14 2002

Publication series

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

Other

Other22nd International Conference on the Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2002
Country/TerritoryIndia
CityKanpur
Period12/12/0212/14/02

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Dynamic Message Sequence charts'. Together they form a unique fingerprint.

Cite this