Statistical Model Checking

SMC can identify mechanistic structures and important regulators in addition to fitting time-course curves. Statistical model checking estimates whether stochastic behavior induced by uncertain initial conditions and parameters satisfies BLTL specifications with specified error guarantees. SMC is framed as a sequential hypothesis test for threshold probability properties. SMC samples trajectories by drawing from INIT, simulating the ODE, and recording whether the BLTL property is satisfied. The same SMC framework was used for parameter estimation, validation, sensitivity analysis, and approximate verification across biological case studies.