Reasoning about sequential and branching behaviours of message sequence graphs

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. © 2011 Springer-Verlag Berlin Heidelberg.