We introduce a context-dependent probabilistic execution structure strictly extending classical probabilistic transition systems. Unlike Segala systems [14], transition probabilities in our model may depend on execution context, represented as histories. We establish a strict non-embeddability theorem showing that classical probabilistic transition systems cannot capture such context-dependent behaviour. We then construct trace semantics via measurable trace spaces in the sense of Giry [4] and prove a final coalgebra representation theorem following standard coalgebraic methodology [13]. Furthermore, we derive a canonical minimal realisation through trace equivalence, yielding a probabilistic Myhill-Nerode theorem. Finally, we prepare the ground for modal and first-order logical characterisations developed in subsequent sections.
huiwenhan•1h ago