Leveraging System-Level Observations to Inform Bayesian Learning of Model Parameters for Quantitative Verification

The paper introduces EPIK, a method for improving Bayesian quantitative verification when prior knowledge about formal model transition parameters is inaccurate or unavailable. Instead of eliciting priors directly over transitions, EPIK uses system-level properties that are observable and connected to real-world semantics. It formulates a twofold optimization problem to infer distributions for unknown transition parameters, then incorporates those distributions into verification of new or difficult-to-measure properties. The abstract reports evaluation across multiple variants of real-world case studies and diverse EPIK instantiations, claiming effectiveness, flexibility, and generality.