Abstraction for Stochastic Systems by Erlang's Method of Stages

Abstract

This paper proposes a novel abstraction technique based on Erlang’s method of stages for continuous-time Markov chains (CTMCs). As abstract models Erlang-kinterval 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.

@inproceedings{katoenAbstractionForStochasticSystems2008,
 author = {Joost-Pieter Katoen and Daniel Klink and Martin Leucker and Verena Wolf},
 booktitle = {CONCUR 2008 - Concurrency Theory. International Conference on Concurrency Theory (CONCUR-2008), 19th International Conference, CONCUR 2008, August 19-22, Toronto, Canada},
 doi = {10.1007/978-3-540-85361-9_24},
 edition = {1st},
 editor = {Franck van Breugel and Marsha Chechik},
 isbn = {9783540853619},
 month = {8},
 pages = {279-294},
 publisher = {Springer Berlin Heidelberg, Heidelberg},
 title = {Abstraction for Stochastic Systems by Erlang's Method of Stages},
 volume = {5201},
 year = {2008}
}