Syntax, Semantics, Equivalences, and Axioms for MTIPP

The stochastic process algebra MTIPP has emerged from research in the field of process descriptions for random behaviour through time. This calculus has recently been shown to allow the calculation of performance measures (e.g. response times), purely functional statements (e.g. occurrences of deadlocks), as well as combined statements (e.g. optimal timeout values) [9, 11]. In contrast to classical process calculi each atomic action is supposed to happen after a delay that is characterised by a certain exponentially distributed random variable. In this report we present the language together with its operational semantics, that defines Markovian labelled transition systems as a combination of classical action-oriented transition systems and Markovian processes, especially continuous time Markov chains. In order to reflect different behavioural aspects we define a hierarchy of bisimulation equivalences and show that two of them are congruences. Finally we present equational laws for our..