In: Lecture Notes in Computer Science, Vol. 1945: Integrated Formal Methods, pages 420-439. Springer-Verlag, 2000.
Abstract: Stochastic processes algebras have been proven useful because they allow behavior-oriented performance and reliability modeling. As opposed to traditional performance modeling techniques, the behavior-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 paradigm hampers the acceptance of the process algebraic approach by performance modelers. This paper develops an entirely behavior-oriented analysis technique for stochastic process algebras. The key contribution is an action-based temporal logic to describe behaviors-of-interest, together with a model checking algorithm to derive the probability with which a stochastic process algebra model exhibits a given behavior-of-interest.
Keywords: behavior-oriented performance, model checking, reliability modeling, stochastic process algebras, temporal logics.