Abstract We provide a fine classification of bisimilarities between states of possibly different labelled Markov processes (LMP). We show that a bisimilarity relation proposed by Panangaden that uses direct sums coincides with “event bisimilarity” from his joint work with Danos, Desharnais, and Laviolette. We also extend Giorgio Bacci’s notions of bisimilarity between two different processes to the case of nondeterministic LMP and generalize the game characterization of state bisimilarity by Clerc et al. for the latter.

Let F = F, R be a finite Kripke frame.A congruence of F is a bisimulation of F that is also an equivalence relation on F. The set of all congruences of F is a lattice under the inclusion ordering.In this article we investigate this lattice in the case that F is a finite line frame.We give concrete descriptions of the join and meet of two congruences with a nontrivial upper bound.Through these descriptions we show that for every nontrivial congruence ρ, the interval [Id F , ρ] embeds into the lattice of divisors of a suitable positive integer.We also prove that any two congruences with a nontrivial upper bound permute.

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.

We prove that the relation of bisimilarity between countable labelled transition systems (LTS) is Σ11-complete (hence not Borel), by reducing the set of non-well orders over the natural numbers continuously to it. This has an impact on the theory of probabilistic and non-deterministic processes over uncountable spaces, since logical characterizations of bisimilarity (as, for instance, those based on the unique structure theorem for analytic spaces) require a countable logic whose formulas have measurable semantics. Our reduction shows that such a logic does not exist in the case of image-infinite processes.

We extend the theory of labelled Markov processes to include internal non-determinism, which is a fundamental concept for the further development of a process theory with abstraction on non-deterministic continuous probabilistic systems. We define non-deterministic labelled Markov processes (NLMP) and provide three definitions of bisimulations: a bisimulation following a traditional characterisation; a state-based bisimulation tailored to our ‘measurable’ non-determinism; and an event-based bisimulation. We show the relations between them, including the fact that the largest state bisimulation is also an event bisimulation. We also introduce a variation of the Hennessy–Milner logic that characterises event bisimulation and is sound with respect to the other bisimulations for an arbitrary NLMP. This logic, however, is infinitary as it contains a denumerable . We then introduce a finitary sublogic that characterises all bisimulations for an image finite NLMP whose underlying measure space is also analytic. Hence, in this setting, all the notions of bisimulation we consider turn out to be equal. Finally, we show that all these bisimulation notions are different in the general case. The counterexamples that separate them turn out to be non-probabilistic NLMPs.