Compositional Methods for Probabilistic Systems

Abstract. We present a compositional trace-based model for probabilistic systems. The behavior of a system with probabilistic choice is a stochasticprocess, namely, a probability distribution on traces, or \bundle." Consequently,thesemanticsofa systemwithbothnondeterministic and probabilistic choice is a set of bundles. The bundles of a composite system can be obtained by combining the bundles of the components in a simple mathematical way. Re nement between systems is bundle containment. We achieve assume-guarantee compositionality for bundle semanticsby introducing two scoping mechanisms. The rst mechanism, which is standard in compositional modeling, distinguishes inputs from outputs and hidden state. The second mechanism, which arises in probabilistic systems, partitions the state into probabilistically independent regions.

• Type: Conference
• Year: 2001
• Where: CONCUR
• Authors: Luca de Alfaro, Thomas A. Henzinger, Ranjit Jhala
• Keywords: CONCUR 2001, Distributed And Parallel Computing, Probabilistic, Probabilistic Choice, Probabilistic Systems