## Compositional Methods for Probabilistic Systems

*Luca de Alfaro,
Thomas A. Henzinger,
and Ranjit Jhala*

We present a compositional trace-based model for probabilistic systems. The
behavior of a system with probabilistic choice is a stochastic process,
namely, a probability distribution on traces, or "bundle." Consequently, the
semantics of a system with both nondeterministic 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.
Refinement between systems is bundle containment. We achieve
assume-guarantee compositionality for bundle semantics by introducing two
scoping mechanisms. The first 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.

*Proceedings of the
12th International Conference on Concurrency Theory*
(CONCUR),
Lecture Notes in Computer Science 2154,
Springer, 2001, pp. 351-365.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2000 Springer.