Behaviour of Labelled Markov Processes Labelled Markov Processes (LMP) seem to be a generalization of Probabilistic Automata (PA) studied by Segala to the case of the general state space. Namely, any LMP is given by a be a finite set of labels $A$, a measurable state space $(X,\mathscr B(X))$ and substochastic kernels
$$
  \forall a\in A,\;\tau_a:X\times \mathscr B(X)\to [0,1].
$$
In case $X$ is finite and $\mathscr B(X) = 2^X$, we obtain simply a PA.

The behavior of the PA is clear to me: it is given by trace distributions over the sequences of labels - e.g. in Section 3 here. I would expect the very same definition of the behavior for LMP, but I have never seen it defined formally anywhere. I would appreciate if you can hint upon a source describing the behaviour of a LMP.

Updated: after a short discussion, I have to clarify some details. I am familiar with measure-theoretical approach to probability and stochastic processes, and I think that behavioral semantics of PA extends directly to LMP modulo dealing with Borel or universally measurable transition kernels to characterize an adversary. However, I am not sure whether this is a possible way to define a behavior of LMP, or it is the intended one. For example, it may perhaps be described in the PhD thesis of J. Desharnais (which I do not have an access to).
[Comment space was too short]

I think it depends on what you mean by behaviour. Probabilistic automata follow in the tradition of finite automata, so their behaviour is defined in terms of their language or traces. Labelled Markov Processes follow in the tradition of process algebra, where it is known that processes can be compared using a variety of preorders typically starting with bisimulation. You do have notions of bisimulation defined for LMPs and in that paper. Bisimulation is stronger than trace equivalence, as you may know, so the behaviour you are interested in is the tree unfolding rooted at a given state. Definition 3.1 of the paper you have linked gives approximations of this tree.