P$$^3$$MC: Towards Probabilistic Programming Probabilistic Model Checking for Linear Temporal Logic

We introduce P^3MC, a novel approach that bridges probabilistic programming and probabilistic model checking for Linear Temporal Logic (LTL). Our framework leverages probabilistic programs as a modeling formalism for stochastic dynamical systems, enabling the analysis of temporal properties at the program level. In particular, we consider the probabilistic programming language SOGA in its DeGAS variant, which approximates program semantics through mixtures of Gaussians. We address the problem of verifying LTL properties over their executions, restricting attention to the past fragment of LTL without the since operator. We propose two complementary model checking techniques. The first approach encodes the LTL monitoring procedure directly within SOGA, allowing property evaluation to be performed alongside program execution under the approximate semantics. This method is highly general and applicable to a wide range of models and properties, but may incur significant computational overhead and approximation error. The second approach targets a restricted, yet practically relevant, class of systems and properties. By statically extracting an approximation of the joint distribution of system states across time, we reduce model checking of reachability and safety properties to the computation of multivariate Gaussian integrals over suitable regions. To this end, we employ an analytical approximation and a numerical method that enable efficient and scalable evaluation. Together, these contributions provide a first step toward a unified framework for probabilistic programming-based model checking, combining the expressiveness of probabilistic programs with the rigor of temporal verification.