Talk "Sound and Complete Axiomatization for Infinite Probabilistic Trace Semantics"

by Ana Sokolova

Sat, 14 June 2025 at 03:00 pm in Glasgow, Scotland

Joint work with: Corina Cirstea, Larry Moss, Tori Noquez, Todd Schmidt, Alexandra Silva

Abstract: This talk is about recent results on axiomatizing infinite trace semantics, also called stream semantics, for generative probabilistic transition systems, also called labelled Markov chains. Axiomatizations work as follows: (states of) probabilistic transition systems can be represented by suitable probabilistic expressions, with the property that the expression and the transition system (state) have the same (in this case trace) semantics. We then provide equations on these expressions that fully characterize infinite trace semantics: two expressions are trace equivalent iff they are provably equivalent with the presented axioms. The axioms for finite traces have been given by Silva and myself in 2011. The soundness and completeness proof is coalgebraic. In recent work with the group of coathors mentioned above, we present the first sound and complete axiomatization of infinite trace semantics. Our approach is categorical, and we build on recent results on proper functors over convex sets - in particular on a novel and simpler proof of properness of the involved functor. At the core of our proof is a characterization of infinite traces as the final coalgebra of a functor over convex algebras. Somewhat surprisingly, our axiomatization of infinite trace semantics coincides with that of finite trace semantics, even though the techniques used in the completeness proof are different.