Stochastic Nondeterminism and Effectivity Functions

TL;DR

This paper explores the relationship between stochastic nondeterminism and effectivity functions on continuous state spaces, establishing connections between different models and defining bisimilarity and logical characterizations.

Contribution

It introduces a formal link between nondeterministic kernels and effectivity functions, and extends bisimulation and logical analysis to these models.

Findings

Effectivity functions mapping into principal filters correspond to image-countable nondeterministic kernels.

Image-finite kernels induce effectivity functions, enabling bisimilarity definitions.

Logical characterization of bisimilarity is provided in the finitary case.

Abstract

This paper investigates stochastic nondeterminism on continuous state spaces by relating nondeterministic kernels and stochastic effectivity functions to each other. Nondeterministic kernels are functions assigning each state a set o subprobability measures, and effectivity functions assign to each state an upper-closed set of subsets of measures. Both concepts are generalizations of Markov kernels used for defining two different models: Nondeterministic labelled Markov processes and stochastic game models, respectively. We show that an effectivity function that maps into principal filters is given by an image-countable nondeterministic kernel, and that image-finite kernels give rise to effectivity functions. We define state bisimilarity for the latter, considering its connection to morphisms. We provide a logical characterization of bisimilarity in the finitary case. A generalization of congruences (event bisimulations) to effectivity functions and its relation to the categorical presentation of bisimulation are also studied.