Trace Semantics for Stochastic Systems with Nondeterminism

Abstract

This paper discusses trace semantics of interactive Markov chains (IMCs) that are a generalisation of continuous-time Markov chains. In IMCs besides probabilistic alternatives there may be a nondeterministic choice between several action-labelled transitions in a state. We analyse several variants of trace equivalences that arise from the different ways one has to resolve nondeterministic branching. Button pushing testing scenarios are used to motivate each abstraction level induced by the trace semantics and associated equivalences are sorted according to their distinguishing power.

@article{wolfTraceSemanticsForStochastic2006,
 author = {Verena Wolf and Christel Baier and Mila Majster-Cederbaum},
 doi = {10.1016/j.entcs.2006.07.019},
 editor = {Nicht bekannt},
 journal = {Electronic Notes in Theoretical Computer Science},
 month = {10},
 number = {3},
 pages = {187-204},
 publisher = {Elsevier, Amsterdam},
 title = {Trace Semantics for Stochastic Systems with Nondeterminism},
 volume = {164},
 year = {2006}
}