PCSP# Denotational Semantics with an Application in Sports Analytics

The chapter introduces probabilistic CSP# (PCSP#) as a formal language for modeling probabilistic systems, emphasizing its foundational role in concurrent and parallel computation. PCSP# is an extension of communicating sequential programs (CSP#) that enables the modeling of probabilistic behaviors and uncertainties in system designs. We provide the formal syntax and denotational semantics for PCSP# based on the UTP framework. We also introduce the Process Analysis Toolkit (PAT) as a formal modeling and verification tool for complex concurrent and probabilistic systems, particularly focusing on its extension CSP# and its variant, PCSP#. The chapter explores the applications of PCSP# in sports analytics, specifically in modeling tennis matches. It demonstrates how PCSP# can be used to analyze match outcomes, develop strategies, and provide training recommendations based on past match data. Experimental results from historical data in the past decade show that formal methods applied to sports analytics yield high-performance and accurate models that are explainable and suitable for strategy and training recommendations.