Probabilistic Configuration Theories

We introduce a new framework for describing computations which are both concurrent and probabilistic. This framework is a natural extension of the Configuration Theories of [Pietro Cenciarelli. Configuration theories. In CSL '02: Proceedings of the 16th International Workshop and 11th Annual Conference of the EACSL on Computer Science Logic, pages 200–215, London, UK, 2002. Springer-Verlag], and allows to express properties about both the causal and the probabilistic aspect of concurrent computations. Computations are described in an axiomatic way, by using a probabilistic extensions of poset sequents. A scheme of structural rules on these sequents is introduced and shown to be sound, while completeness can be obtained by adding a rule which is not treated in the present work. We also introduce a new probabilistic extension of Configuration Structures, which we use as models for probabilistic sequents.