Quantitative Model Checking and Synthesis

点击翻译按钮获取中文摘要

This PhD project will complement work carried out as part of the 3-year Leverhulme-funded research project COVER (COalgebraic Foundations for Quantitative VERification), by studying coalgebraic quantitative logics and their associated verification techniques. The PhD student will work alongside the COVER research team (two academics and two PDRAs) to extend existing quantitative logics and develop associated model checking and synthesis algorithms which are parametric in the type of quantitative model. This work will ultimately extend the applicability of model checking and synthesis techniques to complex systems with a range of correctness and optimality guarantees. The techniques developed as part of the PhD will be evaluated on case studies from the autonomous systems domain.