Causal dependencies in parallel composition of stochastic processes

Abstract. We present some new perspectives on an old problem: com-positionality of trace-style semantics for stochastic processes. The ini-tial step is a more ne-grained analysis of how parallel composition of stochastic processes can be dened in a meaningful way. We make a connection between the notion of adversary models and the formal def-initions of stochastic system types and parallel composition operators. In particular, we focus on causal dependencies arising from the so-called strong adversaries and argue that trace-style semantic compositionality cannot be achieved under strong adversaries. We identify a structural feature of stochastic processes called \invisible probabilistic branching " and illustrate its connection with strong adver-saries. Based on these observations, we introduce a new system type together with appropriate notions of observable behavior and parallel composition. We prove a nite approximation theorem for behaviors and use that to prove semantic compositionality. Finally, we present a model of the Chor-Israeli-Li consensus protocol in our new framework