Learning and Verification
Complex engineering systems, such as autonomous vehicles, are often safety-critical and demand high guarantees of correctness. Given a complete model of the system of interest, these guarantees can be obtained through formal methods, such as model checking, though the outcomes of these formal proofs are bound to the model of the system of interest. Obtaining a complete model is not possible for systems with uncertain stochastic dynamics, but we can capture these dynamics with parameterised Markov chains. Model checking now produces a result dependent on knowledge of the value of parameters within the model.
In this work we integrate the use of model checking techniques (for parameter synthesis over the model) with data-based approaches (for parametric Bayesian inference) in order to compute a confidence, based on observed data collected from the system, that the system satisfies a given specification.
Themes: Learning and Verification
People: Viraj Wijesuriya, Gareth Molyneux, Alessandro Abate
Publications:
- Automated Experiment Design for Data-Efficient Verification of Parametric Markov Decision Processes, , Quantitative Evaluation of Systems - 14th International Conference, {QEST} 2017, Berlin, Germany, September 5-7, 2017, Proceedings, p.259–274, (2017)
- Data-Efficient Bayesian Verification of Parametric Markov Chains, , Quantitative Evaluation of Systems - 13th International Conference, {QEST} 2016, Quebec City, QC, Canada, August 23-25, 2016, Proceedings, p.35–51, (2016)
GET IN TOUCH WITH US
CONTACT US
Oxford Control and Verification (OXCAV) Group
C/O Department of Computer Science
Wolfson Building, Parks Rd, Oxford OX1 3QD
T: +44 (0) 18656 10767
Education - This is a contributing Drupal Theme
Design by WeebPal.
Design by WeebPal.