Causal Message Sequence Charts

Abstract. Scenario languages based on Message Sequence Charts (MSCs) and related notations have been widely studied in the last decade [14, 13, 2, 9, 6, 12, 8]. The high expressive power of scenarios ren-ders many basic problems concerning these languages undecidable. The most expressive class for which several problems are known to be decid-able is one which possesses a behavioral property called “existentially bounded”. However, scenarios outside this class are frequently exhib-ited by asynchronous distributed systems such as sliding window proto-cols. We propose here an extension of MSCs called Causal Message Se-quence Charts, which preserves decidability without requiring existential bounds. Interestingly, it can also model scenarios from sliding window protocols. We establish the expressive power and complexity of decision procedures for various subclasses of Causal Message Sequence Charts.