Working Seminar on Formal Models, Discrete Structures, and Algorithms

Continuous-time Message Sequence Graphs

Clemens Dubslaff (Technische Universität Dresden)

When: Monday February 15, 2pm

Where: room C417 (at the very end of the corridor)


Message sequence charts (MSCs) and their higher-order formalism in terms of message sequence graphs (MSGs) provide an intuitive way to describe communication scenarios and are first and foremost used in early design phases of communication systems. Naturally, quantitative aspects such as the probability of failure, the maximal latency or the expected energy consumption play a crucial role for communication systems. We introduce a continuous-time Markov chain (CTMC) semantics for MSGs and incorporate quantitative information which can be used for a quantitative analysis. For this, we propose a branching-time semantics for MSGs interpreting delayed choice on the partial-order semantics of MSGs. Whereas for locally synchronized MSGs a finite-state bisimulation quotient can be found and thus, standard model-checking algorithms for CTMCs can be applied for a quantitative analysis, this is not the case in general. However, using a truncation-based approach we show how approximative solutions can be obtained. An implementation shows feasibility of this approach exploiting reliability, resilience and energy consumption.