|
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.
[.pdf]
|