technical report Modular probabilistic logic for compositional Harsanyi type spaces


Harsanyi type spaces are general probabilistic structures that have been used as semantics for probabilistic logics, as, for example, with the Aumann system. These type spaces generalize several probabilistic models, such as generative probabilistic automata, labelled Markov processes and, in general, probabilistic transition systems. In this paper we define compositionality over the class of type spaces, enabling it with an algebraic structure that encodes a general notion of synchronization of type spaces. The algebra of type spaces is used as semantics for a logic that extends the Aumann system with structural operators. Using this logic, modular and concurrent probabilistic properties of type spaces can be expressed. This logic can thus be seen as a probabilistic extension of spatial or separation logic as well as a structural extension of probabilistic logic. We present a complete axiomatization and prove the finite model property.

Paper Details


R. Mardare,  I. Mura