Reasoning about sequential and branching behaviours of message sequence graphs

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

Abstract

We study the model-checking problem of message-sequence graphs (MSGs). In the sequential setting, we consider the set of messagesequence charts (MSCs) represented by an MSG and tackle specifications given in monadic second-order logic. We show that this problem, without any restrictions on the MSGs, is decidable. We then turn to branching behaviours of MSGs, define a notion of an unfolding of an MSG, and show that the model-checking problem on unfoldings is also decidable. Our results are stronger and imply that, over an appropriate universe, satisfiability and synthesis of MSCs and MSGs, respectively, are decidable.

Original languageEnglish (US)
Title of host publicationAutomata, Languages and Programming - 28th International Colloquium, ICALP 2001, Proceedings
EditorsFernando Orejas, Paul G. Spirakis, Jan van Leeuwen
PublisherSpringer-Verlag Berlin Heidelberg
Pages809-820
Number of pages12
ISBN (Print)3540422870, 9783540422877
DOIs
StatePublished - Jan 1 2001
Externally publishedYes
Event28th International Colloquium on Automata, Languages and Programming, ICALP 2001 - Crete, Greece
Duration: Jul 8 2001Jul 12 2001

Publication series

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

Other

Other28th International Colloquium on Automata, Languages and Programming, ICALP 2001
CountryGreece
CityCrete
Period7/8/017/12/01

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Reasoning about sequential and branching behaviours of message sequence graphs'. Together they form a unique fingerprint.

Cite this