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

arXiv: https://arxiv.org/abs/2608.03489 · HTML: https://mlsanity.com/paper/2608.03489/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 18 of its 95 references that are in the map.
- First posted on arXiv 4 Aug 2026.

## Builds on (most cited first, 18 of 18)

- [Label-Free Supervision of Neural Networks with Physics and Domain Knowledge](https://mlsanity.com/paper/1609.05566/) (2016)
- [On Testing Machine Learning Programs](https://mlsanity.com/paper/1812.02257/) (2018)
- [A storm is Coming: A Modern Probabilistic Model Checker](https://mlsanity.com/paper/1702.04311/) (2017)
- [Engineering Trustworthy Self-Adaptive Software with Dynamic Assurance Cases](https://mlsanity.com/paper/1703.06350/) (2017)
- [Probabilistic Model Checking of Robots Deployed in Extreme Environments](https://mlsanity.com/paper/1812.04128/) (2018)
- [Assessing Safety-Critical Systems from Operational Testing: A Study on Autonomous Vehicles](https://mlsanity.com/paper/2008.09510/) (2020)
- [Accelerating Parametric Probabilistic Verification](https://mlsanity.com/paper/1312.3979/) (2013)
- [Fast Parametric Model Checking through Model Fragmentation](https://mlsanity.com/paper/2102.01490/) (2021)
- [Bayesian Learning for the Robust Verification of Autonomous Robots](https://mlsanity.com/paper/2303.08476/) (2023)
- [Specification, Validation and Verification of Social, Legal, Ethical, Empathetic and Cultural Requirements for Autonomous Agents](https://mlsanity.com/paper/2307.03697/) (2023)
- [Embedding and Extraction of Knowledge in Tree Ensemble Classifiers](https://mlsanity.com/paper/2010.08281/) (2020)
- [Efficient Parametric Model Checking Using Domain Knowledge](https://mlsanity.com/paper/1812.09952/) (2018)
- [Towards Integrating Formal Verification of Autonomous Robots with Battery Prognostics and Health Management](https://mlsanity.com/paper/1909.03019/) (2019)
- [Adaptive Human-Robot Collaborative Missions using Hybrid Task Planning](https://mlsanity.com/paper/2504.06746/) (2025)
- [Asymptotic Bounds for Quantitative Verification of Perturbed Probabilistic Systems](https://mlsanity.com/paper/1304.7614/) (2013)
- [PRESTO: Predicting System-level Disruptions through Parametric Model Checking](https://mlsanity.com/paper/2205.03628/) (2022)
- [Accelerating Policy Synthesis in Large-Scale MDPs via Hierarchical Adaptive Refinement](https://mlsanity.com/paper/2506.17792/) (2025)
- [Mind the Prompt: Self-adaptive Generation of Task Plan Explanations via LLMs](https://mlsanity.com/paper/2604.21092/) (2026)

## Abstract (arXiv)

Combining Bayesian learning and quantitative verification is a powerful toolset for analysing key quantitative properties of software systems, like reliability and response time. However, the accuracy and robustness of verification results strongly depend on the prior knowledge (PK) underlying Bayesian inference. This knowledge reflects original beliefs about the probability of events and typically depends on domain expertise. Using inaccurate or uninformative PK can negatively affect quantitative analysis, yielding incorrect verification results. Our EPIK approach tackles this important challenge by eliciting and embedding PK in quantitative verification equipped with Bayesian estimators. Unlike existing approaches that require PK on formal model transition parameters, EPIK leverages system-level properties that are directly observable and are linked to real-world semantics. EPIK formulates a twofold optimisation problem to derive the distributions of unknown transition parameters and then embeds these distributions to verify new or difficult-to-measure (elusive) properties. The detailed experimental evaluation using multiple variants of real-world case studies and diverse EPIK instantiations shows its effectiveness, flexibility and generality.