A Demonic Approach to Information in Probabilistic Systems

We establish a duality between specifications and infLMPs. An infLMP is a probabilistic process whose transitions satisfy super-additivity instead of additivity. Interestingly,  its simple structure can encode a mix of probabilistic and non-deterministic behaviors, and is strongly related to another well-known such model:  probabilistic automata.  Our duality puts in relation the category of infLMPs and a category of abstract representations of them based on properties only. We exhibit a Galois connection between these categories  and show that we have an adjunct pair of functors  when restricted to LMPs only. 

Our duality also  shows that an infLMP can be considered as a demonic representative of a system's information. Moreover, it carries forward a view where states are less important, and events, or properties, become the main characters, as it should be in probability theory. Along the way, we show that bisimulation and simulation are naturally interpreted in this setting, and we exhibit the interesting relationship between infLMPs and the usual probabilistic modal logics.