The opposite of \mathsf {FinStoch} [efr-0030]

Recall that (perhaps by definition, perhaps as a trivial theorem, depending on our choice of definition), there is a faithful functor \mathsf {FinStoch} \to \mathsf {Vect} carrying a set X to the vector space \mathbb {R}\langle X \rangle freely generated by X, and a stochastic map f: X \to Y to the map which takes the basis vector x \in X to the linear combination \sum _{y \in Y} y f(y|x). The essential image of this functor is, of course, the finite-dimensional vector spaces. The morphisms in the image are the stochastic matrices, which can be characterized as those that are positive (they carry vectors with positive coordinates to other such vectors) and preserve the constant 1 vector (note that neither of these properties are invariant under isomorphism of finite-dimensional vector space).

One way to think about this is that it proves \mathsf {FinStoch} is equivalent to the category of finite-dimensional, ordered, pointed vector spaces, where we assume that the chosen point must be positive in the order. (To see the inclusion is essentially surjective, note that given a vector space pointed by (a_1, \dots a_n), all those coordinates positive, it receives an isomorphism from the same spaces pointed by (1, \dots 1) given by the diagonal matrix with entries a_1, \dots a_n).

Now, let \mathsf {fdVect}^\leq denote the category of finite-dimensional ordered vector spaces. Then equipping a space V with a positive point is exactly choosing an order-preserving linear map \mathbb {R} \to V, so we have proven \mathsf {FinStoch} \simeq \mathsf {fdVect}^\leq _{ \mathbb {R} /}. Now we can compute \mathsf {FinStoch}^\mathrm {op} \simeq (\mathsf {fdVect}^\leq _{ \ RR/})^\mathrm {op} \cong (\mathsf {fdVect}^\leq )^\mathrm {op}_{ / \mathbb {R}} \cong \mathsf {fdVect}^\leq _{ / \mathbb {R}}, where the last isomorphism is via transposition (note that transposing a positive matrix yields a positive matrix).

This isomorphism merely describes the fact that stochastic maps \phi : X \to Y can also be described as linear maps f: \mathbb {R}\langle Y \rangle \to \mathbb {R}\langle X \rangle so that \sum _x f((a_y))_x = \sum _y a_y. This map interprets a vector as a function on Y, and carries it to the function on X which finds the expected value if y \in Y is distributed as \phi (x). The normalization condition merely says a constant function always has that constant as its expectation.

The self-duality of \mathsf {fdVect} does not generalize to infinite-dimensional vector spaces, so once we move beyond finite state spaces, this story will get somewhat more complicated. However, the basic idea that, to carry the tools of coalgebraic modal logic into the stochastic case, the sort of "predicate" we should consider is actually a function on the state space, will remain the central idea.

(Indeed, to consider the right notion of stochastic function between, for example, smooth manifolds, we will in any case want to use the tools of functional analysis to think of these in terms of transformation on integration operators, which is essentially this idea).

Another way to justify this idea is to note that \Omega = \{\bot ,\top \} is the subobject classifier for \mathsf {Fin} \subseteq \mathsf {FinStoch}. Hence if we want our notion of predicate to transform under stochastic maps, and include the logical predicates in the usual sense, we have to at least consider the stochastic maps X \to \Omega , which of course amount to functions X \to [0,1] in this case. But a positive linear map on functions is determined by what it does to functions like this, so whether we work only with these or all functions X \to \mathbb {R} is more or less a matter of taste.

Instead of having a logic consisting of the operations of Boolean algebra, augmented with extra operations described by T^\mathrm {op} B \to B, we have the operations of a vector space, augmented by some extra modal operations. The Markov structure of \mathsf {FinStoch}, or whichever category we work in, will give the vector space of functions an \mathbb {R}-algebra structure, but we should note that some equations fail to hold in general (dual to the fact that not all morphisms in the Markov category are homomorphisms for the comonoid structure). The Hennessy-Milner property is essentially the same in this situation, saying that our set of modally-expressible functions should separate points in the terminal coalgebra. Since we will have multiplication and linear combinations of functions, this entails under some mild topological conditions that it's dense in the set of functions on the terminal coalgebra.

It is worth examining this analogy a bit further, in the simpler setup of coalgebraic modal logic. If X is a space in some general sense, let us schematically write C(X) for the space of functions on X, so that as above stochastic maps X \to Y are identified with certain linear maps C(Y) \to C(X). Again, the Markov structure on the category of stochastic maps (whatever it is) amounts to the fact that C(X) carries the structure of an \mathbb {R}-algebra, and deterministic maps are those which are not algebra homomorphisms.

Let now \xi : X \to A \otimes X be a simple stochastic dynamical system which outputs a value of type A at each step. The dual of this is C(A) \otimes C(X) \to C(X), where the tensor here is now the tensor product of vector spaces.

Among algebras, the tensor product is the coproduct, so we may restrict the above map to form two modal operators, C(A) \to C(X) and C(X) \to C(X)---the latter being simply the transition operator taking a function \phi (x) to the expected value of the next step, the former computing the expected value of the output given x. But since the transition may be nondeterministic, these two restrictions do not determine it. From a logical point of view, the problem is that we can't express statements about the correlation between the output and the next step.

As a simple counterexample, consider two system where X = A = \{0,1\}. In the first, the output and the next state are independent, and both equal the current state with probability 1-\epsilon . In the other, the output and next state are always equal, and again are equal to the current state with probability 1-\epsilon

These systems have the same marginals X \to A and X \to X, and hence the two modal operators above have the same behaviour, and hence every modally expressible function is the same. But in the former, the probability of seeing ab output sequence beginning 1,0,\dots when starting in state 0 is proportional to \epsilon , whereas in the latter it is proportional to \epsilon ^2 (since you have to flip twice), so these systems have very different behaviour.

Using § [efr-000X], we can deduce a version of Hennessy-Milner for stochastic transition systems (with no input and outputs in finite set A). Namely, fix a system \xi : X \to A \otimes X, and let \nabla (u,v), with u: A \to \mathbb {R} and v: X \to \mathbb {R} denote the function which carries x \in X to the expected value of u(a)v(x') when (a,x') are distributed according to the system. Then \nabla is precisely the bilinear function C(A) \otimes C(X) \to C(X) dual to \xi . Since A^\omega is the terminal coalgebra, and the inverse limit of A \leftarrow A^2 \leftarrow \dots , we can infer that C(A^\omega ) is the colimit of the sequence C(A) \to C(A) \otimes C(A) \to \dots in some category of \mathbb {R}-algebras (we must think a little about topology to make this precise.)

But this should imply that the union of the images of C(A)^{\otimes n} inside this algebra is dense. So certainly they separate points. But this image consists exactly of formulas given by functions on A, applications of \nabla , and sums and products. So these formulae are sufficiently expressive to separate points of the terminal coalgebra (which are, of course, exactly bisimulation classes).