A logical duality for underspecified probabilistic systems (Q532396)

A simple structure, infLMP (essentially partial specification of labeled Markov processes), that encodes non-determinism and probabilistic behaviour (its transitions satisfy super-additivity instead of additivity) is introduced. A Stone-type duality between specifications and imfLMP is established. The duality puts in relation the category of infLMPs and a category of abstract representations of them based on properties only. A Galois connection between these categories is exhibited. The duality also shows that an imfLMP 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. It is shown that bisimulation and simulation are naturally interpreted in this setting, and the interesting relationship between infLMPs and the usual probabilistic modal logics is exhibited.