We extend the formal developments for message sequence charts (MSCs) to support scenarios with lost and found messages. We define a notion of extended compositional message sequence charts (ECMSCs) which subsumes the notion of compositional message sequence charts in expressive power but additionally allows to define lost and found messages explicitly. As usual, ECMSCs can be combined by means of choice and repetition to (extended) compositional message sequence graphs. We show that--despite extended expressive power--model checking of monadic second-order logic (MSO) for this framework remains to be decidable. The key technique to achieve our results is to use an extended notion for linearizations.
@conference(BLL-LPAR-02-CompositionalMSGs,
author={Benedikt Bollig and Martin Leucker and Philipp Lucas},
title={Extending Compositional Message Sequence Graphs},
booktitle={Proceedings of the 9th International Conference on Logic for
Programming, Artificial Intelligence and Reasoning (LPAR'02)},
pages={68--85},
editor={Matthias Baaz and Andrei Voronkov},
publisher={Springer-Verlag},
series={LNCS},
volume=2514,
year=2002
)
Valid XHTML 1.0 Strict, valid CSS.
Author: Philipp Lucas.