Operator Algebras and the Operational Semantics of Probabilistic Languages

We investigate the construction of linear operators representing the semantics of probabilistic programming languages expressed via probabilistic transition systems. Finite transition relations, corresponding to fi- nite automata, can easily be represented by finite dimensional matrices; for the infinite case we need to consider an appropriate generalisation of matrix algebras. We argue that C∗-algebras, or more precisely Approximately Finite (or AF) algebras, provide a sufficiently rich mathematical structure for modelling probabilistic processes. We show how to construct for a given probabilistic language a unique AF algebra A and how to represent the operational semantics of processes within this framework: finite computations correspond directly to operators in A, while infinite processes are represented by elements in the so-called strong closure of this algebra.