Stochastic process algebras have been proven useful because they allow behaviour-oriented performance and reliability modelling. As opposed to traditional performance modelling techniques, the behaviour- oriented style supports composition and abstraction in a natural way. However, analysis of stochastic process algebra models is state-oriented, because standard numerical analysis is typically based on the calculation of (transient and steady) state probabilities. This shift of paradigms hampers the acceptance of the process algebraic approach by performance modellers. In this paper, we develop an entirely behaviour-oriented analysis technique for stochastic process algebras. The key contribution is an action-based temporal logic to describe behaviours-of-interest, together with a model checking algorithm to derive the probability with which a stochastic process algebra model exhibits a given behaviour-of-interest. © Springer-Verlag Berlin Heidelberg 2000.
CITATION STYLE
Hermanns, H., Katoen, J. P., Meyer-Kayser, J., & Siegle, M. (2000). Towards model checking stochastic process algebra. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1945 LNCS, pp. 420–439). Springer Verlag. https://doi.org/10.1007/3-540-40911-4_24
Mendeley helps you to discover research relevant for your work.