Comparative Linear-Time Semantics on Action-Labelled Continuous-Time Markov Chains

Abstract

Extended Abstract: Comparative linear-time semantics like (maximal/finite) trace and readiness/failure equivalence have been widely considered for labelled transition systems (for an overview see [vG90]) and also in the (discrete-time) probabilistic setting [DTH92, Seg95]. We extend these semantics to the stochastic setting by considering them for action-labelled continuous-time Markov chains (aCTMCs), the underlying model of stochastic process algebras [BG96, Hil96, NGR92]. Similar to probabilistic processes, transitions occur with a certain probability. Additionally, each state has an associated residence time given by an exponentially distributed random variable. ACTMCs can also been seen as an action-labelled extension of continuous-time Markov chains, a standard model used in performance analysis [Ste95]. We present several equivalence relations on aCTMCs that have, to the best of our knowledge, not yet been defined and analysed in this way. Although in many cases equivalences based on the linear-time structure provide the best abstraction for verification purposes, most work on stochastic extensions of labelled transition systems is restricted to equivalences based on the branching-time structure of a process (an overview is given in [CBW03]). We extend the testing scenario of [vG90, SV03] to the stochastic setting to motivate our semantics by considering the following experiment: Intuitively, two aCTMCs are considered as “equal” if they can not be distinguished by observing the sequence of performed actions (trace) in infinitely many runs. Assume that an aCTMC M is modelled as a black box (stochastic trace machine …

@inproceedings{wolfComparativeLinearTimeSemanticsOn2004,
 author = {Verena Wolf and Christel Baier},
 booktitle = {Proceedings of the 16th Nordic Workshop on Programming Theory. Nordic Workshop on Programming Theory, October 6-8, Uppsala, Sweden},
 editor = {Paul Pettersson and Wang Yi},
 month = {10},
 pages = {80-82},
 publisher = {Department of Information Technology, Uppsala University},
 series = {Technical Report},
 title = {Comparative Linear-Time Semantics on Action-Labelled Continuous-Time Markov Chains},
 volume = {2004-041},
 year = {2004}
}