Trace Machines for Observing Continuous-Time Markov Chains

Verena WolfVerena Wolf, Christel BaierChristel Baier, Mila E. Majster-CederbaumMila E. Majster-Cederbaum

DOI Link

Verena Wolf, Christel Baier, Mila E. Majster-Cederbaum
Trace Machines for Observing Continuous-Time Markov Chains
Proc. of the Third Workshop on Quantitative Aspects of Programming Languages (QAPL), volume 153(2) of Electronic Notes in Theoretical Computer Science, 259--277, 2005. Elsevier

Details
Bibtex

KurzfassungAbstract
In this paper, we study several linear-time equivalences (Markovian trace equivalence, failure and ready trace equivalence) for continuous-time Markov chains that refer to the probabilities for timed execution paths. Our focus is on testing scenarios by means of push-button experiments with appropriate trace machines and a discussion of the connections between the equivalences. For Markovian trace equivalence, we provide alternative characterizations, including one that abstracts away from the time instances where actions are observed, but just reports on the average sojourn times in the states. This result is used for a reduction of the question whether two finite-state continuous-time Markov chains are Markovian trace equivalent to the probabilistic trace equivalence problem for discrete-time Markov chains (and the latter is known to be solvable in polynomial time).
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{WBM2005,
  author    = {Verena Wolf and Christel Baier and Mila E. Majster-Cederbaum},
  title     = {Trace Machines for Observing Continuous-Time Markov Chains},
  booktitle = {Proc. of the Third Workshop on Quantitative Aspects of
               Programming Languages (QAPL)},
  series    = {Electronic Notes in Theoretical Computer Science},
  volume    = {153(2)},
  publisher = {Elsevier},
  year      = {2005},
  pages     = {259--277},
  doi       = {10.1016/J.ENTCS.2005.10.042}
}