@inproceedings{Dam2007,
Author = {Damm, Werner and Toben, Tobe and Westphal, Bernd},
Title = {On the Expressive Power of Live Sequence Charts},

Year = {2007},
Pages = {225-246},
Month = {01},
Publisher = {Springer Verlag},
Series = {LNCS},
Edition = {4444},
Booktitle = {Program Analysis and Compilation, Theory and Practise: Essays Dedicated to Reinhard Wilhelm},
type = {inproceedings},
note = {The Live Sequence Charts (LSC) language is a formally rigorous variant of the well-known scenario language Message Sequence Charts (MSC). LSCs yield expressive power by means to distinguish mandatory and scenario behaviour, means to characterise by anothe},
Abstract = {The Live Sequence Charts (LSC) language is a formally rigorous variant of the well-known scenario language Message Sequence Charts (MSC). LSCs yield expressive power by means to distinguish mandatory and scenario behaviour, means to characterise by another scenario the context in which a specification applies, and means to distinguish required from possible progress, i.e. to require liveness. From the original proposal by Damm and Harel, two slightly different dialects emerged, one in the context of LSC play-in and -out and one for the use of LSCs as formal, model-based approaches to software development. In this paper, we first (constructively) show that for each LSC there is an equivalent CTL* formula. Complementing existing work, we show that the containment is strict, that is, not each CTL* formula has an equivalent LSC. To complete the discussion, we present for the first time a way back, from a syntactically characterised fragment of CTL* to the subset of bonded LSC specifications, thereby establishing an equivalence.}
}
@COMMENT{Bibtex file generated on }