Quantitative Model Checking and Synthesis

这个博士项目将通过研究coalgebraic定量逻辑及其相关的验证技术，补充作为为期3年的Leverhulme资助的研究项目COVER（定量验证的COalgebraic基础）的一部分进行的工作。该博士生将与COVER研究团队（两名学者和两名PDRA）合作，扩展现有的定量逻辑并开发相关的模型检查和合成算法，这些算法在定量模型类型中是参数化的。这项工作将最终扩展模型检查和合成技术的适用性，复杂的系统与一系列的正确性和最优性保证。作为博士学位的一部分开发的技术将在自治系统领域的案例研究中进行评估。

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.