The following technical report is available from http://aib.informatik.rwth-aachen.de:
Abstraction for stochastic systems by Erlang's method of stages Joost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf AIB 2008-12
This paper proposes a novel abstraction technique based on Erlang's method of stages for continuous-time Markov chains (CTMCs). As abstract models Erlang-k interval processes are proposed where state residence times are governed by Poisson processes and transition probabilities are specified by intervals. We provide a three-valued semantics of CSL (Continuous Stochastic Logic) for Erlang-k interval processes, and show that both affirmative and negative verification results are preserved by our abstraction. The feasibility of our technique is demonstrated by a quantitative analysis of an enzyme-catalyzed substrate conversion, a well-known case study from biochemistry.